(VAR X) (RULES f(X,g(X)) -> f(1,g(X)) g(1) -> g(0) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend