Consider the TRS R consisting of the rewrite rules

1: minus(x,0) -> x
2: minus(s(x),s(y)) -> minus(x,y)
3: quot(0,s(y)) -> 0
4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
5: le(0,y) -> true
6: le(s(x),0) -> false
7: le(s(x),s(y)) -> le(x,y)
8: app(nil,y) -> y
9: app(add(n,x),y) -> add(n,app(x,y))
10: low(n,nil) -> nil
11: low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
12: if_low(true,n,add(m,x)) -> add(m,low(n,x))
13: if_low(false,n,add(m,x)) -> low(n,x)
14: high(n,nil) -> nil
15: high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
16: if_high(true,n,add(m,x)) -> high(n,x)
17: if_high(false,n,add(m,x)) -> add(m,high(n,x))
18: quicksort(nil) -> nil
19: quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))

There are 18 dependency pairs:

20: MINUS(s(x),s(y)) -> MINUS(x,y)
21: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
22: QUOT(s(x),s(y)) -> MINUS(x,y)
23: LE(s(x),s(y)) -> LE(x,y)
24: APP(add(n,x),y) -> APP(x,y)
25: LOW(n,add(m,x)) -> IF_LOW(le(m,n),n,add(m,x))
26: LOW(n,add(m,x)) -> LE(m,n)
27: IF_LOW(true,n,add(m,x)) -> LOW(n,x)
28: IF_LOW(false,n,add(m,x)) -> LOW(n,x)
29: HIGH(n,add(m,x)) -> IF_HIGH(le(m,n),n,add(m,x))
30: HIGH(n,add(m,x)) -> LE(m,n)
31: IF_HIGH(true,n,add(m,x)) -> HIGH(n,x)
32: IF_HIGH(false,n,add(m,x)) -> HIGH(n,x)
33: QUICKSORT(add(n,x)) -> APP(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
34: QUICKSORT(add(n,x)) -> QUICKSORT(low(n,x))
35: QUICKSORT(add(n,x)) -> LOW(n,x)
36: QUICKSORT(add(n,x)) -> QUICKSORT(high(n,x))
37: QUICKSORT(add(n,x)) -> HIGH(n,x)

The approximated dependency graph contains 7 SCCs:
{24},
{23},
{29,31,32},
{25,27,28},
{20},
{34,36}
and {21}.

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

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

- Consider the SCC {29,31,32}.
The usable rules are {5-7}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[add](x,y) = [HIGH](x,y) = [le](x,y) = x + y + 1
and [IF_HIGH](x,y,z) = y + z + 1,
rule 29
is weakly decreasing and
the rules in {5-7,31,32}
are strictly decreasing.

- Consider the SCC {25,27,28}.
The usable rules are {5-7}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[add](x,y) = [le](x,y) = [LOW](x,y) = x + y + 1
and [IF_LOW](x,y,z) = y + z + 1,
rule 25
is weakly decreasing and
the rules in {5-7,27,28}
are strictly decreasing.

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

- Consider the SCC {34,36}.
The usable rules are {5-7,10-17}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[QUICKSORT](x) = [s](x) = x + 1,
[high](x,y) = x + y,
[add](x,y) = [le](x,y) = [low](x,y) = x + y + 1,
[if_high](x,y,z) = y + z
and [if_low](x,y,z) = y + z + 1,
the rules in {11,12,14,15,17,34}
are weakly decreasing and
the rules in {5-7,10,13,16,36}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {34}.
The usable rules are {5-7,10-13}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[QUICKSORT](x) = [s](x) = x + 1,
[low](x,y) = x + y,
[add](x,y) = [le](x,y) = x + y + 1
and [if_low](x,y,z) = y + z,
the rules in {10-12}
are weakly decreasing and
the rules in {5-7,13,34}
are strictly decreasing.


- Consider the SCC {21}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = x,
[s](x) = x + 1
and [QUOT](x,y) = x + y + 1,
rule 1
is weakly decreasing and
the rules in {2,21}
are strictly decreasing.

Hence the TRS is terminating.