Consider the TRS R consisting of the rewrite rules

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

There are 2 dependency pairs:

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

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

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

Hence the TRS is terminating.