YES
(VAR x)
(RULES 
f(a,x) -> f(g(x),x)
h(g(x)) -> h(a)
g(h(x)) -> g(x)
h(h(x)) -> x
)

Proving termination of rewriting for improved_usable2:

-> Dependency pairs:
nF_f(a,x) -> nF_f(g(x),x)
nF_f(a,x) -> nF_g(x)
nF_h(g(x)) -> nF_h(a)
nF_g(h(x)) -> nF_g(x)

-> Proof of termination for improved_usable2_1_1:
-> -> Dependency pairs in cycle:
nF_f(a,x) -> nF_f(g(x),x)

UsableRules:
g(h(x)) -> g(x)

Polynomial Interpretation:

[f](X1,X2) = 0
[a] = 1
[g](X) = 0
[h](X) = 0
[nF_f](X1,X2) = X1

TIME: 5.1269e-2


-> Proof of termination for improved_usable2_1_2:
-> -> Dependency pairs in cycle:
nF_g(h(x)) -> nF_g(x)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.