Consider the TRS R consisting of the rewrite rules

1: le(0,Y) -> true
2: le(s(X),0) -> false
3: le(s(X),s(Y)) -> le(X,Y)
4: app(nil,Y) -> Y
5: app(cons(N,L),Y) -> cons(N,app(L,Y))
6: low(N,nil) -> nil
7: low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
8: iflow(true,N,cons(M,L)) -> cons(M,low(N,L))
9: iflow(false,N,cons(M,L)) -> low(N,L)
10: high(N,nil) -> nil
11: high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
12: ifhigh(true,N,cons(M,L)) -> high(N,L)
13: ifhigh(false,N,cons(M,L)) -> cons(M,high(N,L))
14: quicksort(nil) -> nil
15: quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))

There are 15 dependency pairs:

16: LE(s(X),s(Y)) -> LE(X,Y)
17: APP(cons(N,L),Y) -> APP(L,Y)
18: LOW(N,cons(M,L)) -> IFLOW(le(M,N),N,cons(M,L))
19: LOW(N,cons(M,L)) -> LE(M,N)
20: IFLOW(true,N,cons(M,L)) -> LOW(N,L)
21: IFLOW(false,N,cons(M,L)) -> LOW(N,L)
22: HIGH(N,cons(M,L)) -> IFHIGH(le(M,N),N,cons(M,L))
23: HIGH(N,cons(M,L)) -> LE(M,N)
24: IFHIGH(true,N,cons(M,L)) -> HIGH(N,L)
25: IFHIGH(false,N,cons(M,L)) -> HIGH(N,L)
26: QUICKSORT(cons(N,L)) -> APP(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
27: QUICKSORT(cons(N,L)) -> QUICKSORT(low(N,L))
28: QUICKSORT(cons(N,L)) -> LOW(N,L)
29: QUICKSORT(cons(N,L)) -> QUICKSORT(high(N,L))
30: QUICKSORT(cons(N,L)) -> HIGH(N,L)

The approximated dependency graph contains 5 SCCs:
{17},
{16},
{22,24,25},
{18,20,21}
and {27,29}.

- Consider the SCC {17}.
There are no usable rules.
By taking the polynomial interpretation
[APP](x,y) = [cons](x,y) = x + y + 1,
rule 17
is strictly decreasing.

- Consider the SCC {16}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [LE](x,y) = x + y + 1,
rule 16
is strictly decreasing.

- Consider the SCC {22,24,25}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[cons](x,y) = [HIGH](x,y) = [le](x,y) = x + y + 1
and [IFHIGH](x,y,z) = y + z + 1,
rule 22
is weakly decreasing and
the rules in {1-3,24,25}
are strictly decreasing.

- Consider the SCC {18,20,21}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[cons](x,y) = [le](x,y) = [LOW](x,y) = x + y + 1
and [IFLOW](x,y,z) = y + z + 1,
rule 18
is weakly decreasing and
the rules in {1-3,20,21}
are strictly decreasing.

- Consider the SCC {27,29}.
The usable rules are {1-3,6-13}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[QUICKSORT](x) = [s](x) = x + 1,
[high](x,y) = x + y,
[cons](x,y) = [le](x,y) = [low](x,y) = x + y + 1,
[ifhigh](x,y,z) = y + z
and [iflow](x,y,z) = y + z + 1,
the rules in {7,8,10,11,13,27}
are weakly decreasing and
the rules in {1-3,6,9,12,29}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {27}.
The usable rules are {1-3,6-9}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[QUICKSORT](x) = [s](x) = x + 1,
[low](x,y) = x + y,
[cons](x,y) = [le](x,y) = x + y + 1
and [iflow](x,y,z) = y + z,
the rules in {6-8}
are weakly decreasing and
the rules in {1-3,9,27}
are strictly decreasing.


Hence the TRS is terminating.