Consider the TRS R consisting of the rewrite rules

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

There are 4 dependency pairs:

3: (x * y) +# (a * y) -> (x + a) *# y
4: (x * y) +# (a * y) -> x +# a
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}.
The usable rules are {2}.
By taking the polynomial interpretation
[*](x,y) = [*#](x,y) = x + y + 1,
the rules in {2,5}
are weakly decreasing and
rule 6
is strictly decreasing.
There is one new SCC.

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


Hence the TRS is terminating.