Consider the TRS R consisting of the rewrite rules

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

There are 3 dependency pairs:

4: F(s(x),s(y)) -> F(x,y)
5: G(0,x) -> G(f(x,x),x)
6: G(0,x) -> F(x,x)

The approximated dependency graph contains 2 SCCs:
{4}
and {5}.

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

- Consider the SCC {5}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[f](x,y) = [s](x) = 0,
[0] = 1
and [G](x,y) = x + y + 1,
the rules in {1,2}
are weakly decreasing and
rule 5
is strictly decreasing.

Hence the TRS is terminating.