(COMMENT reversing lists)
(VAR x y l orig accu)
(RULES
length(nil) -> 0
length(cons(x,l)) -> s(length(l))
lt(x,0) -> false
lt(0,s(y)) -> true
lt(s(x),s(y)) -> lt(x,y)
head(cons(x,l)) -> x
head(nil) -> undefined
tail(nil) -> nil
tail(cons(x,l)) -> l

reverse(l) -> rev(0,l,nil,l)
rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
if(true,x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
if(false,x,l,accu,orig) -> accu
)