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