(COMMENT harder variant of AG01 3.38)
(VAR x y l)
(RULES
empty(nil) -> true
empty(cons(x,l)) -> false
head(cons(x,l)) -> x
tail(nil) -> nil
tail(cons(x,l)) -> l
rev(nil) -> nil
rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
last(x,l) -> if(empty(l),x,l)
if(true,x,l) -> x
if(false,x,l) -> last(head(l),tail(l))
rev2(x,nil) -> nil
rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
)