Consider the TRS R consisting of the rewrite rules

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

There are 4 dependency pairs:

5: G(x,s(y)) -> G(f(x,y),0)
6: G(s(x),y) -> G(f(x,y),0)
7: G(f(x,y),0) -> G(x,0)
8: G(f(x,y),0) -> G(y,0)

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

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

Hence the TRS is terminating.