Consider the TRS R consisting of the rewrite rules

1: rev(a) -> a
2: rev(b) -> b
3: rev(x ++ y) -> rev(y) ++ rev(x)
4: rev(x ++ x) -> rev(x)

There are 3 dependency pairs:

5: REV(x ++ y) -> REV(y)
6: REV(x ++ y) -> REV(x)
7: REV(x ++ x) -> REV(x)

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

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

Hence the TRS is terminating.