Cut Elimination - ComputerAidedLL/click-and-collect Wiki

Try to predict the result before asking the machine to reduce the cut.

Then you can use Undo/Redo buttons to replay.

Key Cases

Commutative Cases

Confluence

Try to get two different cut-free proofs by reducing the cut in the following proofs:

Additive Booleans

Exponential Isomorphism