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