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