(VAR l l1 l2 x )
(STRATEGY INNERMOST)
(RULES 
        is_empty(nil) -> true
        is_empty(cons(x,l)) -> false
        hd(cons(x,l)) -> x
        tl(cons(x,l)) -> cons(x,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))
        
)