(VAR X XS) (RULES zeros -> cons(0,zeros) tail(cons(X,XS)) -> XS )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend