(VAR YS X XS Y L) (RULES app(nil,YS) -> YS app(cons(X),YS) -> cons(X) from(X) -> cons(X) zWadr(nil,YS) -> nil zWadr(XS,nil) -> nil zWadr(cons(X),cons(Y)) -> cons(app(Y,cons(X))) prefix(L) -> cons(nil) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend