(COMMENT Claude Marché List append with auxiliary functions (currently fails with CiME) ) (VAR l2 l1 l 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)) )