Consider the TRS R consisting of the rewrite rules

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

There are 2 dependency pairs:

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

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

- Consider the SCC {4}.
By taking the polynomial interpretation
[0] = 0,
[s](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {1-3}
are weakly decreasing and
rule 4
is strictly decreasing.

Hence the TRS is terminating.