Consider the TRS R consisting of the rewrite rule

1: a(b(a(x))) -> b(a(b(x)))

There is one dependency pair:

2: A(b(a(x))) -> A(b(x))

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

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

Hence the TRS is terminating.