Consider the TRS R consisting of the rewrite rules

1: x * (y * z) -> (x * y) * z
2: x * x -> x

There are 2 dependency pairs:

3: x *# (y * z) -> (x * y) *# z
4: x *# (y * z) -> x *# y

The approximated dependency graph contains one SCC:
{3,4}.

- Consider the SCC {3,4}.
By taking the polynomial interpretation
[*](x,y) = [*#](x,y) = x + y + 1,
the rules in {1,3}
are weakly decreasing and
the rules in {2,4}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {3}.
By taking the polynomial interpretation
[*](x,y) = x + y + 1
and [*#](x,y) = y + 1,
rule 1
is weakly decreasing and
the rules in {2,3}
are strictly decreasing.


Hence the TRS is terminating.