(VAR x y z) (RULES app(app(*, x), app(app(+, y), z)) -> app(app(+, app(app(*, x), y)), app(app(*, x), z)) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend