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: less_leaves(x,leaf) -> false
4: less_leaves(leaf,cons(w,z)) -> true
5: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))

There are 4 dependency pairs:

6: CONCAT(cons(u,v),y) -> CONCAT(v,y)
7: LESS_LEAVES(cons(u,v),cons(w,z)) -> LESS_LEAVES(concat(u,v),concat(w,z))
8: LESS_LEAVES(cons(u,v),cons(w,z)) -> CONCAT(u,v)
9: LESS_LEAVES(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) = [LESS_LEAVES](x,y) = x + y + 1,
rule 2
is weakly decreasing and
the rules in {1,7}
are strictly decreasing.

Hence the TRS is terminating.