YES
(VAR x y)
(RULES 
cond(true,x,y) -> cond(gr(x,y),p(x),s(y))
gr(0,x) -> false
gr(s(x),0) -> true
gr(s(x),s(y)) -> gr(x,y)
p(0) -> 0
p(s(x)) -> x
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for 2:

-> Dependency pairs:
nF_cond(true,x,y) -> nF_cond(gr(x,y),p(x),s(y))
nF_cond(true,x,y) -> nF_gr(x,y)
nF_cond(true,x,y) -> nF_p(x)
nF_gr(s(x),s(y)) -> nF_gr(x,y)

-> Proof of termination for 2_1_1:
-> -> Dependency pairs in cycle:
nF_cond(true,x,y) -> nF_cond(gr(x,y),p(x),s(y))

UsableRules:
gr(0,x) -> false
gr(s(x),0) -> true
gr(s(x),s(y)) -> gr(x,y)
p(0) -> 0
p(s(x)) -> x

Polynomial Interpretation:

[cond](X1,X2,X3) = 0
[true] = 1
[gr](X1,X2) = 1/2.X1
[p](X) = 1/2.X
[s](X) = 2.X + 2
[0] = 0
[false] = 0
[nF_cond](X1,X2,X3) = 2.X1 + 2.X2

TIME: 3.116e-3


-> Proof of termination for 2_1_2:
-> -> Dependency pairs in cycle:
nF_gr(s(x),s(y)) -> nF_gr(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.