(COMMENT 

  Claude Marché

  List append with auxiliary functions

)


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