(VAR l l1 l2 x )
(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))
        
)