def Cslib.CLL.Proof.cutFree {Atom : Type u} {Γ : Sequent Atom} (p : Logic.InferenceSystem.derivation Γ) : Bool

A proof is cut-free if it does not contain any applications of rule cut.

Equations

• Cslib.CLL.Proof.ax.cutFree = true
• Cslib.CLL.Proof.one.cutFree = true
• p_2.bot.cutFree = p_2.cutFree
• p_2.parr.cutFree = p_2.cutFree
• (p_2.tensor q).cutFree = (p_2.cutFree && q.cutFree)
• p_2.oplus₁.cutFree = p_2.cutFree
• p_2.oplus₂.cutFree = p_2.cutFree
• (p_2.with q).cutFree = (p_2.cutFree && q.cutFree)
• Cslib.CLL.Proof.top.cutFree = true
• p_2.quest.cutFree = p_2.cutFree
• p_2.weaken.cutFree = p_2.cutFree
• p_2.contract.cutFree = p_2.cutFree
• (Cslib.CLL.Proof.bang a_1 p_2).cutFree = p_2.cutFree
• (a_1.cut a_2).cutFree = false

@[reducible, inline]

abbrev Cslib.CLL.CutFreeProof {Atom : Type u} (Γ : Sequent Atom) : Type u

A CutFreeProof is a Proof without cuts (applications of Proof.cut).

Equations

• Cslib.CLL.CutFreeProof Γ = { q : Cslib.Logic.InferenceSystem.derivation Γ // Cslib.CLL.Proof.cutFree q = true }