Consider the TRS R consisting of the rewrite rules

1: g(h(g(x))) -> g(x)
2: g(g(x)) -> g(h(g(x)))
3: h(h(x)) -> h(f(h(x),x))

There are 3 dependency pairs:

4: G(g(x)) -> G(h(g(x)))
5: G(g(x)) -> H(g(x))
6: H(h(x)) -> H(f(h(x),x))

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

- Consider the SCC {4}.
By taking the polynomial interpretation
[h](x) = 0,
[g](x) = 1,
[G](x) = x + 1
and [f](x,y) = x + y + 1,
the rules in {1-3}
are weakly decreasing and
rule 4
is strictly decreasing.

Hence the TRS is terminating.