(VAR a d x k) (RULES f(a,empty) -> g(a, empty) f(a,cons(x,k)) -> f(cons(x,a), k) g(empty,d) -> d g(cons(x,k),d) -> g(k, cons(x,d)))
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend