Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

11: I(x + y) -> i(x) +# i(y)
12: I(x + y) -> I(x)
13: I(x + y) -> I(y)
14: x +# (y + z) -> (x + y) +# z
15: x +# (y + z) -> x +# y

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

- Consider the SCC {14,15}.
The usable rules are {2,3,5,6,8-10}.
By taking the polynomial interpretation
[0] = 1,
[i](x) = x + 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {8,14}
are weakly decreasing and
the rules in {2,3,5,6,9,10,15}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {14}.
By taking the polynomial interpretation
[0] = 1,
[i](x) = x + 1,
[+](x,y) = x + y + 1
and [+#](x,y) = y + 1,
rule 8
is weakly decreasing and
the rules in {2,3,5,6,9,10,14}
are strictly decreasing.


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

Hence the TRS is terminating.