(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, l1) ifappend(l1, l2, nil) -> l2 ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) )