YES
(VAR x y)
(RULES 
g(x,0) -> 0
g(d,s(x)) -> s(s(g(d,x)))
g(h,s(0)) -> 0
g(h,s(s(x))) -> s(g(h,x))
double(x) -> g(d,x)
half(x) -> g(h,x)
f(s(x),y) -> f(half(s(x)),double(y))
f(s(0),y) -> y
id(x) -> f(x,s(0))
)

Proving termination of rewriting for identity:

-> Dependency pairs:
nF_g(d,s(x)) -> nF_g(d,x)
nF_g(h,s(s(x))) -> nF_g(h,x)
nF_double(x) -> nF_g(d,x)
nF_half(x) -> nF_g(h,x)
nF_f(s(x),y) -> nF_f(half(s(x)),double(y))
nF_f(s(x),y) -> nF_half(s(x))
nF_f(s(x),y) -> nF_double(y)
nF_id(x) -> nF_f(x,s(0))

-> Dependency pairs narrowed: 
nF_f(s(x),y) -> nF_f(half(s(x)),double(y))

-> New dependency pairs: 
nF_f(s(x),y) -> nF_f(g(h,s(x)),double(y))

-> Proof of termination for identity_1_1:
-> -> Dependency pairs in cycle:
nF_f(s(x),y) -> nF_f(g(h,s(x)),double(y))

UsableRules:
g(x,0) -> 0
g(d,s(x)) -> s(s(g(d,x)))
g(h,s(0)) -> 0
g(h,s(s(x))) -> s(g(h,x))
double(x) -> g(d,x)

Polynomial Interpretation:

[g](X1,X2) = X1.X2
[0] = 0
[d] = 2
[s](X) = X + 2
[h] = 1/2
[double](X) = 2.X
[half](X) = 0
[f](X1,X2) = 0
[id](X) = 0
[nF_f](X1,X2) = 2.X1

TIME: 0.260353


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

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for identity_1_3:
-> -> Dependency pairs in cycle:
nF_g(d,s(x)) -> nF_g(d,x)

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: Simple mixed
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.