Consider the TRS R consisting of the rewrite rules

1: times(x,0) -> 0
2: times(x,s(y)) -> plus(times(x,y),x)
3: plus(x,0) -> x
4: plus(0,x) -> x
5: plus(x,s(y)) -> s(plus(x,y))
6: plus(s(x),y) -> s(plus(x,y))

There are 4 dependency pairs:

7: TIMES(x,s(y)) -> PLUS(times(x,y),x)
8: TIMES(x,s(y)) -> TIMES(x,y)
9: PLUS(x,s(y)) -> PLUS(x,y)
10: PLUS(s(x),y) -> PLUS(x,y)

The approximated dependency graph contains 2 SCCs:
{9,10}
and {8}.

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

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

Hence the TRS is terminating.