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

Proving termination of rewriting for jwttt:

-> Dependency pairs:
nF_f(x,f(a,y)) -> nF_f(a,f(f(a,h(f(a,x))),y))
nF_f(x,f(a,y)) -> nF_f(f(a,h(f(a,x))),y)
nF_f(x,f(a,y)) -> nF_f(a,h(f(a,x)))
nF_f(x,f(a,y)) -> nF_f(a,x)

-> Dependency pairs narrowed: 
nF_f(x,f(a,y)) -> nF_f(a,f(f(a,h(f(a,x))),y))

-> New dependency pairs: 
nF_f(x,f(a,f(a,y))) -> nF_f(a,f(a,f(f(a,h(f(a,f(a,h(f(a,x)))))),y)))

-> Proof of termination for jwttt_1:
-> -> Dependency pairs in cycle:
nF_f(x,f(a,y)) -> nF_f(f(a,h(f(a,x))),y)
nF_f(x,f(a,f(a,y))) -> nF_f(a,f(a,f(f(a,h(f(a,f(a,h(f(a,x)))))),y)))
nF_f(x,f(a,y)) -> nF_f(a,x)

UsableRules:
f(x,f(a,y)) -> f(a,f(f(a,h(f(a,x))),y))

Polynomial Interpretation:

[f](X1,X2) = 2.X2 + 2
[a] = 0
[h](X) = 0
[nF_f](X1,X2) = 2.X1 + 2.X2

TIME: 2.96e-4

-> -> Dependency pairs in cycle:
nF_f(x,f(a,y)) -> nF_f(f(a,h(f(a,x))),y)
nF_f(x,f(a,f(a,y))) -> nF_f(a,f(a,f(f(a,h(f(a,f(a,h(f(a,x)))))),y)))

UsableRules:
f(x,f(a,y)) -> f(a,f(f(a,h(f(a,x))),y))

Polynomial Interpretation:

[f](X1,X2) = 1/2.X1 + 2.X2
[a] = 2
[h](X) = 0
[nF_f](X1,X2) = 2.X2

TIME: 1.22e-3

-> -> Dependency pairs in cycle:
nF_f(x,f(a,y)) -> nF_f(f(a,h(f(a,x))),y)

Termination proved: Cycles verify subterm criterion.

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



Termination was proved succesfully.