(VAR x) (RULES app(f, app(g, x)) -> app(g, app(g, app(f, x))) app(f, app(g, x)) -> app(g, app(g, app(g, x))) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend