Consider the TRS R consisting of the rewrite rules

1: 0 + y -> y
2: s(x) + y -> s(x + y)
3: s(x) + y -> x + s(y)

There are 2 dependency pairs:

4: s(x) +# y -> x +# y
5: s(x) +# y -> x +# s(y)

The approximated dependency graph contains one SCC:
{4,5}.

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

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


Hence the TRS is terminating.