Consider the TRS R consisting of the rewrite rules

1: x * (y * z) -> otimes(x,y) * z
2: 1 * y -> y
3: (x + y) * z -> oplus(x * z,y * z)
4: x * oplus(y,z) -> oplus(x * y,x * z)

There are 5 dependency pairs:

5: x *# (y * z) -> otimes(x,y) *# z
6: (x + y) *# z -> x *# z
7: (x + y) *# z -> y *# z
8: x *# oplus(y,z) -> x *# y
9: x *# oplus(y,z) -> x *# z

The approximated dependency graph contains one SCC:
{5-9}.

- Consider the SCC {5-9}.
There are no usable rules.
By taking the polynomial interpretation
[*](x,y) = [*#](x,y) = [+](x,y) = [oplus](x,y) = [otimes](x,y) = x + y + 1,
rule 5
is weakly decreasing and
the rules in {6-9}
are strictly decreasing.
There is one new SCC.

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


Hence the TRS is terminating.