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

Proving termination of rewriting for jwtpa2:

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

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

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

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

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

Polynomial Interpretation:

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

TIME: 3.01e-4

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

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

Polynomial Interpretation:

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

TIME: 0.20047199999999998

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

Termination proved: Cycles verify subterm criterion.

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



Termination was proved succesfully.