Consider the TRS R consisting of the rewrite rules

1: merge(nil,y) -> y
2: merge(x,nil) -> x
3: merge(x . y,u . v) -> if(x < u,x . merge(y,u . v),u . merge(x . y,v))
4: nil ++ y -> y
5: (x . y) ++ z -> x . (y ++ z)
6: if(true,x,y) -> x
7: if(false,x,y) -> x

There are 4 dependency pairs:

8: MERGE(x . y,u . v) -> IF(x < u,x . merge(y,u . v),u . merge(x . y,v))
9: MERGE(x . y,u . v) -> MERGE(y,u . v)
10: MERGE(x . y,u . v) -> MERGE(x . y,v)
11: (x . y) ++# z -> y ++# z

The approximated dependency graph contains 2 SCCs:
{11}
and {9,10}.

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

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

Hence the TRS is terminating.