Consider the TRS R consisting of the rewrite rules

1: f(X) -> g(n__h(n__f(X)))
2: h(X) -> n__h(X)
3: f(X) -> n__f(X)
4: activate(n__h(X)) -> h(activate(X))
5: activate(n__f(X)) -> f(activate(X))
6: activate(X) -> X

There are 4 dependency pairs:

7: ACTIVATE(n__h(X)) -> H(activate(X))
8: ACTIVATE(n__h(X)) -> ACTIVATE(X)
9: ACTIVATE(n__f(X)) -> F(activate(X))
10: ACTIVATE(n__f(X)) -> ACTIVATE(X)

The approximated dependency graph contains one SCC:
{8,10}.

- Consider the SCC {8,10}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [n__f](x) = [n__h](x) = x + 1,
the rules in {8,10}
are strictly decreasing.

Hence the TRS is terminating.