Consider the TRS R consisting of the rewrite rules

1: f(0) -> 1
2: f(s(x)) -> g(f(x))
3: g(x) -> x + s(x)
4: f(s(x)) -> f(x) + s(f(x))

There are 2 dependency pairs:

5: F(s(x)) -> G(f(x))
6: F(s(x)) -> F(x)

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

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

Hence the TRS is terminating.