Cut Elimination

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

Then you can use Undo/Redo buttons to replay.

Key Cases

• ax
• ⊗/⅋
• ⊕₁/&
• ⊕₂/&
• 1/⊥
• !/?d
• !/?c
• !/?w

Commutative Cases

• ⊗
• ⅋
• ⊕₁
• ⊕₂
• &
• ⊥
• ⊤
• ! (including !/!)
• ?d
• ?c
• ?w

Confluence

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

• ⊢ A^, A⊗B, B^⊗C^, C
• ⊢ A⅋B, (A^⊗B^)⊗(C^⊗D^), C⅋D
• ⊢ A&A, A^&A^

Additive Booleans

• not false

Exponential Isomorphism

• Reduce !A⊗!B ⊢ !A⊗!B and compare with !A⊗!B ⊢ !A⊗!B
• Reduce !(A&B) ⊢ !(A&B) and compare with !(A&B) ⊢ !(A&B)