Consider the TRS R consisting of the rewrite rules

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

There are 3 dependency pairs:

5: F(a) -> H(a)
6: H(g(x)) -> H(f(x))
7: H(g(x)) -> F(x)

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

- Consider the SCC {6}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[a] = 1,
[h](x) = 2x - 2,
[H](x) = x,
[f](x) = x + 1
and [g](x) = x + 2,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 6
is strictly decreasing.

Hence the TRS is terminating.