Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

3: A(a(x)) -> B(b(x))
4: A(a(x)) -> B(x)
5: B(b(a(x))) -> A(b(b(x)))
6: B(b(a(x))) -> B(b(x))
7: B(b(a(x))) -> B(x)

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

- Consider the SCC {3-7}.
By taking the polynomial interpretation
[a](x) = [A](x) = [b](x) = [B](x) = x + 1,
the rules in {1-3,5}
are weakly decreasing and
the rules in {4,6,7}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {3,5}.
By taking the polynomial interpretation
[b](x) = x
and [a](x) = [A](x) = [B](x) = x + 1,
rule 2
is weakly decreasing and
the rules in {1,3,5}
are strictly decreasing.


Hence the TRS is terminating.