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