(from AG01 3.38) (VAR x y l) (RULES rev(nil) -> nil rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l)) rev1(0,nil) -> 0 rev1(s(x),nil) -> s(x) rev1(x,cons(y,l)) -> rev1(y,l) rev2(x,nil) -> nil rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l))) )