Consider the TRS R consisting of the rewrite rules

1: rev(ls) -> r1(ls,empty)
2: r1(empty,a) -> a
3: r1(cons(x,k),a) -> r1(k,cons(x,a))

There are 2 dependency pairs:

4: REV(ls) -> R1(ls,empty)
5: R1(cons(x,k),a) -> R1(k,cons(x,a))

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

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

Hence the TRS is terminating.