Consider the TRS R consisting of the rewrite rules

1: f(0) -> s(0)
2: f(s(0)) -> s(s(0))
3: f(s(0)) -> s(s(0)) * f(0)
4: f(x + s(0)) -> s(s(0)) + f(x)
5: f(x + y) -> f(x) * f(y)

There are 4 dependency pairs:

6: F(s(0)) -> F(0)
7: F(x + s(0)) -> F(x)
8: F(x + y) -> F(x)
9: F(x + y) -> F(y)

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

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

Hence the TRS is terminating.