Consider the TRS R consisting of the rewrite rules

1: sort(nil) -> nil
2: sort(cons(x,y)) -> insert(x,sort(y))
3: insert(x,nil) -> cons(x,nil)
4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
5: choose(x,cons(v,w),y,0) -> cons(x,cons(v,w))
6: choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w))
7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)

There are 5 dependency pairs:

8: SORT(cons(x,y)) -> INSERT(x,sort(y))
9: SORT(cons(x,y)) -> SORT(y)
10: INSERT(x,cons(v,w)) -> CHOOSE(x,cons(v,w),x,v)
11: CHOOSE(x,cons(v,w),0,s(z)) -> INSERT(x,w)
12: CHOOSE(x,cons(v,w),s(y),s(z)) -> CHOOSE(x,cons(v,w),y,z)

The approximated dependency graph contains 2 SCCs:
{10-12}
and {9}.

- Consider the SCC {10-12}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1
and [CHOOSE](x,y,z,w) = [cons](x,y) = [INSERT](x,y) = x + y + 1,
the rules in {10,12}
are weakly decreasing and
rule 11
is strictly decreasing.
There is one new SCC.

- Consider the SCC {12}.
By taking the polynomial interpretation
[s](x) = x + 1,
[cons](x,y) = x + y + 1
and [CHOOSE](x,y,z,w) = x + y + z + w + 1,
rule 12
is strictly decreasing.


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

Hence the TRS is terminating.