Consider the TRS R consisting of the rewrite rules

1: merge(x,nil) -> x
2: merge(nil,y) -> y
3: merge(x ++ y,u ++ v) -> x ++ merge(y,u ++ v)
4: merge(x ++ y,u ++ v) -> u ++ merge(x ++ y,v)

There are 2 dependency pairs:

5: MERGE(x ++ y,u ++ v) -> MERGE(y,u ++ v)
6: MERGE(x ++ y,u ++ v) -> MERGE(x ++ y,v)

The approximated dependency graph contains one SCC:
{5}.

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

Hence the TRS is terminating.