(VAR x y z u) (RULES app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) -> app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u)) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend