Consider the TRS R consisting of the rewrite rules

1: msort(nil) -> nil
2: msort(x . y) -> min(x,y) . msort(del(min(x,y),x . y))
3: min(x,nil) -> x
4: min(x,y . z) -> if(x <= y,min(x,z),min(y,z))
5: del(x,nil) -> nil
6: del(x,y . z) -> if(x = y,z,y . del(x,z))

There are 6 dependency pairs:

7: MSORT(x . y) -> MSORT(del(min(x,y),x . y))
8: MSORT(x . y) -> DEL(min(x,y),x . y)
9: MSORT(x . y) -> MIN(x,y)
10: MIN(x,y . z) -> MIN(x,z)
11: MIN(x,y . z) -> MIN(y,z)
12: DEL(x,y . z) -> DEL(x,z)

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

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

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

- Consider the SCC {7}.
The usable rules are {3-6}.
By taking the polynomial interpretation
[=](x,y) = [del](x,y) = [nil] = 0,
[if](x,y,z) = x,
[MSORT](x) = x + 1
and [.](x,y) = [<=](x,y) = [min](x,y) = x + y + 1,
the rules in {5,6}
are weakly decreasing and
the rules in {3,4,7}
are strictly decreasing.

Hence the TRS is terminating.