Consider the TRS R consisting of the rewrite rules

1: concat(leaf,Y) -> Y
2: concat(cons(U,V),Y) -> cons(U,concat(V,Y))
3: lessleaves(X,leaf) -> false
4: lessleaves(leaf,cons(W,Z)) -> true
5: lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

There are 4 dependency pairs:

6: CONCAT(cons(U,V),Y) -> CONCAT(V,Y)
7: LESSLEAVES(cons(U,V),cons(W,Z)) -> LESSLEAVES(concat(U,V),concat(W,Z))
8: LESSLEAVES(cons(U,V),cons(W,Z)) -> CONCAT(U,V)
9: LESSLEAVES(cons(U,V),cons(W,Z)) -> CONCAT(W,Z)

The approximated dependency graph contains 2 SCCs:
{6}
and {7}.

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

- Consider the SCC {7}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[leaf] = 1,
[concat](x,y) = x + y
and [cons](x,y) = [LESSLEAVES](x,y) = x + y + 1,
rule 2
is weakly decreasing and
the rules in {1,7}
are strictly decreasing.

Hence the TRS is terminating.