YES
(VAR x l l1 l2)
(RULES 
is_empty(nil) -> true
is_empty(cons(x,l)) -> false
hd(cons(x,l)) -> x
tl(cons(x,l)) -> l
append(l1,l2) -> ifappend(l1,l2,is_empty(l1))
ifappend(l1,l2,true) -> l2
ifappend(l1,l2,false) -> cons(hd(l1),append(tl(l1),l2))
)

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

-> Dependency pairs:
nF_append(l1,l2) -> nF_ifappend(l1,l2,is_empty(l1))
nF_append(l1,l2) -> nF_is_empty(l1)
nF_ifappend(l1,l2,false) -> nF_hd(l1)
nF_ifappend(l1,l2,false) -> nF_append(tl(l1),l2)
nF_ifappend(l1,l2,false) -> nF_tl(l1)

-> Proof of termination for append_hard_1:
-> -> Dependency pairs in cycle:
nF_append(l1,l2) -> nF_ifappend(l1,l2,is_empty(l1))
nF_ifappend(l1,l2,false) -> nF_append(tl(l1),l2)

UsableRules:
is_empty(nil) -> true
is_empty(cons(x,l)) -> false
tl(cons(x,l)) -> l

Polynomial Interpretation:

[is_empty](X) = X
[nil] = 0
[true] = 0
[cons](X1,X2) = 2.X2 + 2
[false] = 2
[hd](X) = 0
[tl](X) = 1/2.X
[append](X1,X2) = 0
[ifappend](X1,X2,X3) = 0
[nF_append](X1,X2) = 2.X1
[nF_ifappend](X1,X2,X3) = X1 + X3

TIME: 1.0739e-2


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.