Consider the TRS R consisting of the rewrite rule

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

There is one dependency pair:

2: A(b(x)) -> A(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) = [b](x) = x + 1,
rule 2
is strictly decreasing.

Hence the TRS is terminating.