YES
(VAR x y z)
(RULES 
h(x,c(y,z)) -> h(c(s(y),x),z)
h(c(s(x),c(s(0),y)),z) -> h(y,c(s(0),c(x,z)))
)

Proving termination of rewriting for direct:

-> Dependency pairs:
nF_h(x,c(y,z)) -> nF_h(c(s(y),x),z)
nF_h(c(s(x),c(s(0),y)),z) -> nF_h(y,c(s(0),c(x,z)))

-> Proof of termination for direct_1:
-> -> Dependency pairs in cycle:
nF_h(x,c(y,z)) -> nF_h(c(s(y),x),z)
nF_h(c(s(x),c(s(0),y)),z) -> nF_h(y,c(s(0),c(x,z)))

There are no usable rules.

Polynomial Interpretation:

[h](X1,X2) = 0
[c](X1,X2) = 1/2.X1 + X2
[s](X) = 1/2.X
[0] = 1/2
[nF_h](X1,X2) = X1 + 1/2.X2

TIME: 3.54e-4

-> -> Dependency pairs in cycle:
nF_h(x,c(y,z)) -> nF_h(c(s(y),x),z)

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: All rationals
Delta: automatic



Termination was proved succesfully.