Consider the TRS R consisting of the rewrite rules

1: i(x) * x -> 1
2: 1 * y -> y
3: x * 0 -> 0
4: (x * y) * z -> x * (y * z)

There are 2 dependency pairs:

5: (x * y) *# z -> x *# (y * z)
6: (x * y) *# z -> y *# z

The approximated dependency graph contains one SCC:
{5,6}.

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

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


Hence the TRS is terminating.