Consider the TRS R consisting of the rewrite rule

1: x * (minus(y) * y) -> minus(y * y) * x

There are 2 dependency pairs:

2: x *# (minus(y) * y) -> minus(y * y) *# x
3: x *# (minus(y) * y) -> y *# y

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

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

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


Hence the TRS is terminating.