(VAR X Y) (RULES f(X,g(X),Y) -> f(Y,Y,Y) g(b) -> c b -> c )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend