Consider the TRS R consisting of the rewrite rules

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

There are 6 dependency pairs:

9: x +# minus(y) -> MINUS(minus(x) + y)
10: x +# minus(y) -> minus(x) +# y
11: x +# minus(y) -> MINUS(x)
12: x +# (y + z) -> (x + y) +# z
13: x +# (y + z) -> x +# y
14: minus(x + 1) +# 1 -> MINUS(x)

The approximated dependency graph contains one SCC:
{10,12,13}.

- Consider the SCC {10,12,13}.
By taking the polynomial interpretation
[0] = [1] = 1,
[minus](x) = x
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {1,5-7,10,12}
are weakly decreasing and
the rules in {2-4,8,13}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {10,12}.
By taking the polynomial interpretation
[0] = [1] = 1,
[minus](x) = x,
[+](x,y) = x + y + 1
and [+#](x,y) = y + 1,
the rules in {1,5-7,10}
are weakly decreasing and
the rules in {2-4,8,12}
are strictly decreasing.
There is one new SCC.

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



Hence the TRS is terminating.