Consider the TRS R consisting of the rewrite rules

1: f(0) -> 1
2: f(s(x)) -> g(x,s(x))
3: g(0,y) -> y
4: g(s(x),y) -> g(x,y + s(x))
5: x + 0 -> x
6: x + s(y) -> s(x + y)
7: g(s(x),y) -> g(x,s(y + x))

There are 6 dependency pairs:

8: F(s(x)) -> G(x,s(x))
9: G(s(x),y) -> G(x,y + s(x))
10: G(s(x),y) -> y +# s(x)
11: x +# s(y) -> x +# y
12: G(s(x),y) -> G(x,s(y + x))
13: G(s(x),y) -> y +# x

The approximated dependency graph contains 2 SCCs:
{11}
and {9,12}.

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

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

Hence the TRS is terminating.