Consider the TRS R consisting of the rewrite rules

1: qsort(nil) -> nil
2: qsort(x . y) -> qsort(lowers(x,y)) ++ (x . qsort(greaters(x,y)))
3: lowers(x,nil) -> nil
4: lowers(x,y . z) -> if(y <= x,y . lowers(x,z),lowers(x,z))
5: greaters(x,nil) -> nil
6: greaters(x,y . z) -> if(y <= x,greaters(x,z),y . greaters(x,z))

There are 6 dependency pairs:

7: QSORT(x . y) -> QSORT(lowers(x,y))
8: QSORT(x . y) -> LOWERS(x,y)
9: QSORT(x . y) -> QSORT(greaters(x,y))
10: QSORT(x . y) -> GREATERS(x,y)
11: LOWERS(x,y . z) -> LOWERS(x,z)
12: GREATERS(x,y . z) -> GREATERS(x,z)

The approximated dependency graph contains 3 SCCs:
{12},
{11}
and {7,9}.

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

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

- Consider the SCC {7,9}.
The usable rules are {3-6}.
By taking the polynomial interpretation
[<=](x,y) = 0,
[nil] = 1,
[QSORT](x) = x + 1,
[if](x,y,z) = [lowers](x,y) = x + y
and [.](x,y) = [greaters](x,y) = x + y + 1,
the rules in {3,4,9}
are weakly decreasing and
the rules in {5-7}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {9}.
The usable rules are {5,6}.
By taking the polynomial interpretation
[<=](x,y) = 0,
[nil] = 1,
[QSORT](x) = x + 1,
[greaters](x,y) = x + y,
[.](x,y) = x + y + 1
and [if](x,y,z) = x + z,
the rules in {5,6}
are weakly decreasing and
rule 9
is strictly decreasing.


Hence the TRS is terminating.