YES
(VAR x y)
(RULES 
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))
times(0,y) -> 0
times(s(x),y) -> if_times(even(s(x)),s(x),y)
if_times(true,s(x),y) -> plus(times(half(s(x)),y),times(half(s(x)),y))
if_times(false,s(x),y) -> plus(y,times(x,y))
)

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 _4_29:

-> Dependency pairs:
nF_even(s(s(x))) -> nF_even(x)
nF_half(s(s(x))) -> nF_half(x)
nF_plus(s(x),y) -> nF_plus(x,y)
nF_times(s(x),y) -> nF_if_times(even(s(x)),s(x),y)
nF_times(s(x),y) -> nF_even(s(x))
nF_if_times(true,s(x),y) -> nF_plus(times(half(s(x)),y),times(half(s(x)),y))
nF_if_times(true,s(x),y) -> nF_times(half(s(x)),y)
nF_if_times(true,s(x),y) -> nF_half(s(x))
nF_if_times(false,s(x),y) -> nF_plus(y,times(x,y))
nF_if_times(false,s(x),y) -> nF_times(x,y)

-> Dependency pairs narrowed: 
nF_if_times(true,s(x),y) -> nF_times(half(s(x)),y)

-> New dependency pairs: 
nF_if_times(true,s(s(x)),y) -> nF_times(s(half(x)),y)

-> Proof of termination for _4_29_1_1:
-> -> Dependency pairs in cycle:
nF_times(s(x),y) -> nF_if_times(even(s(x)),s(x),y)
nF_if_times(true,s(s(x)),y) -> nF_times(s(half(x)),y)
nF_if_times(false,s(x),y) -> nF_times(x,y)

UsableRules:
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))

Polynomial Interpretation:

[even](X) = X
[0] = 1
[true] = 0
[s](X) = X + 1
[false] = 0
[half](X) = X
[plus](X1,X2) = 0
[times](X1,X2) = 0
[if_times](X1,X2,X3) = 0
[nF_times](X1,X2) = X1
[nF_if_times](X1,X2,X3) = X2

TIME: 4.8694e-2

-> -> Dependency pairs in cycle:
nF_times(s(x),y) -> nF_if_times(even(s(x)),s(x),y)
nF_if_times(true,s(s(x)),y) -> nF_times(s(half(x)),y)

UsableRules:
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))

Polynomial Interpretation:

[even](X) = X
[0] = 1
[true] = 0
[s](X) = X + 1
[false] = 0
[half](X) = X
[plus](X1,X2) = 0
[times](X1,X2) = 0
[if_times](X1,X2,X3) = 0
[nF_times](X1,X2) = X1
[nF_if_times](X1,X2,X3) = X2

TIME: 5.1624e-2


-> Proof of termination for _4_29_1_2:
-> -> Dependency pairs in cycle:
nF_plus(s(x),y) -> nF_plus(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _4_29_1_3:
-> -> Dependency pairs in cycle:
nF_half(s(s(x))) -> nF_half(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _4_29_1_4:
-> -> Dependency pairs in cycle:
nF_even(s(s(x))) -> nF_even(x)

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



Termination was proved succesfully.