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