(VAR X Y) (RULES first(0,X) -> nil first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend