(VAR x y) (RULES app(f, app(s, x)) -> app(f, x) app(g, app(app(cons, 0), y)) -> app(g, y) app(g, app(app(cons, app(s, x)), y)) -> app(s, x) app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y))) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend