(VAR X Y) (RULES f(s(X),Y) -> h(s(f(h(Y),X))) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend