Consider the TRS R consisting of the rewrite rules

1: x + 0 -> x
2: minus(x) + x -> 0
3: minus(0) -> 0
4: minus(minus(x)) -> x
5: minus(x + y) -> minus(y) + minus(x)
6: x * 1 -> x
7: x * 0 -> 0
8: x * (y + z) -> (x * y) + (x * z)
9: x * minus(y) -> minus(x * y)

There are 8 dependency pairs:

10: MINUS(x + y) -> minus(y) +# minus(x)
11: MINUS(x + y) -> MINUS(y)
12: MINUS(x + y) -> MINUS(x)
13: x *# (y + z) -> (x * y) +# (x * z)
14: x *# (y + z) -> x *# y
15: x *# (y + z) -> x *# z
16: x *# minus(y) -> MINUS(x * y)
17: x *# minus(y) -> x *# y

The approximated dependency graph contains 2 SCCs:
{11,12}
and {14,15,17}.

- Consider the SCC {11,12}.
There are no usable rules.
By taking the polynomial interpretation
[MINUS](x) = x + 1
and [+](x,y) = x + y + 1,
the rules in {11,12}
are strictly decreasing.

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

Hence the TRS is terminating.