Consider the TRS R consisting of the rewrite rules

1: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
2: times(X,s(Y)) -> plus(X,times(Y,X))

There are 4 dependency pairs:

3: PLUS(plus(X,Y),Z) -> PLUS(X,plus(Y,Z))
4: PLUS(plus(X,Y),Z) -> PLUS(Y,Z)
5: TIMES(X,s(Y)) -> PLUS(X,times(Y,X))
6: TIMES(X,s(Y)) -> TIMES(Y,X)

The approximated dependency graph contains 2 SCCs:
{3,4}
and {6}.

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

- Consider the SCC {3}.
By taking the polynomial interpretation
[PLUS](x,y) = x + 1
and [plus](x,y) = x + y + 1,
rule 1
is weakly decreasing and
rule 3
is strictly decreasing.


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

Hence the TRS is terminating.