(VAR ls a x k) (RULES rev(ls) -> r1(ls, empty) r1(empty, a) -> a r1(cons(x,k), a) -> r1(k, cons(x,a)))