/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/append-wrong.trs

The program

(COMMENT 

  Claude Marché

  List append with auxiliary functions, wrong version

  (does NOT terminate)


)

(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)) -> 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)) 


)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend