YES
(VAR x l)
(RULES 
is_empty(cons(x,l)) -> false
is_empty(nil) -> true
)

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

-> Dependency pairs:
No dependency pairs found.

-> Proof of termination for append_1:
Termination proved: No cycles in dependency graph.

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

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

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

-> Dependency pairs:
nF_append(l1,l2) -> nF_ifappend(l1,l2,l1)
nF_ifappend(l1,l2,cons(x,l)) -> nF_append(l,l2)

-> Proof of termination for append_2:
-> -> Dependency pairs in cycle:
nF_append(l1,l2) -> nF_ifappend(l1,l2,l1)
nF_ifappend(l1,l2,cons(x,l)) -> nF_append(l,l2)

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.