Consider the TRS R consisting of the rewrite rules

1: plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
2: plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

There are 5 dependency pairs:

3: PLUS(s(X),plus(Y,Z)) -> PLUS(X,plus(s(s(Y)),Z))
4: PLUS(s(X),plus(Y,Z)) -> PLUS(s(s(Y)),Z)
5: PLUS(s(X1),plus(X2,plus(X3,X4))) -> PLUS(X1,plus(X3,plus(X2,X4)))
6: PLUS(s(X1),plus(X2,plus(X3,X4))) -> PLUS(X3,plus(X2,X4))
7: PLUS(s(X1),plus(X2,plus(X3,X4))) -> PLUS(X2,X4)

The approximated dependency graph contains one SCC:
{3-7}.

- Consider the SCC {3-7}.
By taking the polynomial interpretation
[s](x) = x
and [plus](x,y) = [PLUS](x,y) = x + y + 1,
the rules in {1-3,5}
are weakly decreasing and
the rules in {4,6,7}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {3,5}.
By taking the polynomial interpretation
[plus](x,y) = [PLUS](x,y) = [s](x) = x + 1,
the rules in {1-3,5}
are strictly decreasing.


Hence the TRS is terminating.