Consider the TRS R consisting of the rewrite rules

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

There are 4 dependency pairs:

5: F(a,x) -> F(g(x),x)
6: F(a,x) -> G(x)
7: H(g(x)) -> H(a)
8: G(h(x)) -> G(x)

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

- Consider the SCC {8}.
There are no usable rules.
By taking the polynomial interpretation
[G](x) = [h](x) = x + 1,
rule 8
is strictly decreasing.

- Consider the SCC {5}.
The usable rules are {3}.
By taking the polynomial interpretation
[g](x) = 0,
[a] = 1,
[h](x) = x + 1
and [F](x,y) = x + y + 1,
rule 3
is weakly decreasing and
rule 5
is strictly decreasing.

Hence the TRS is terminating.