Theorem: formalStarFormal (Fine/SystemB/Theories.lean)

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
⊢ formalTheory (FormalDual Γ)
Tactic:
intros F
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
⊢ F ∈ FormalDual Γ ↔ FormalDual Γ⊢F

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
⊢ F ∈ FormalDual Γ ↔ FormalDual Γ⊢F
Tactic:
apply Iff.intro <;> intros h₃ <;> unfold FormalDual
State after:
case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F

case mpr
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F
Tactic:
case mp => exact ⟨BProof.ax h₃⟩
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
case mpr =>
  have ⟨prf₁⟩ := h₃
  induction prf₁
  case ax => assumption
  case mp P Q prf₂ thm₁ ih₁ =>
    intros h₄
    have l₁ := ih₁ ⟨prf₂⟩
    unfold FormalDual at l₁
    have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
    have prf₂ := BProof.mp (BProof.ax h₄) thm₂
    exact l₁ (h₁.mpr ⟨prf₂⟩) 
  case adj P Q prf₁ prf₂ ih₁ ih₂ =>
    intros h₄
    have l₁ := ih₁ ⟨prf₁⟩
    have l₂ := ih₂ ⟨prf₂⟩
    have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
    have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
    cases l₃
    case inl left => exact l₁ left
    case inr right => exact l₂ right
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F
Tactic:
exact ⟨BProof.ax h₃⟩
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
have ⟨prf₁⟩ := h₃
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
prf₁ : BProof (FormalDual Γ) F
⊢ F ∈ fun f => ¬~f ∈ Γ

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
prf₁ : BProof (FormalDual Γ) F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
induction prf₁
State after:
case ax
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ

case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢q✝
⊢ q✝ ∈ fun f => ¬~f ∈ Γ

case adj
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BProof (FormalDual Γ) q✝
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₂_ih✝ : FormalDual Γ⊢q✝ → q✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢p✝&q✝
⊢ p✝&q✝ ∈ fun f => ¬~f ∈ Γ

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ
Tactic:
case ax => assumption
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
⊢ Q ∈ fun f => ¬~f ∈ Γ
Tactic:
case mp P Q prf₂ thm₁ ih₁ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₂⟩
  unfold FormalDual at l₁
  have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
  have prf₂ := BProof.mp (BProof.ax h₄) thm₂
  exact l₁ (h₁.mpr ⟨prf₂⟩)
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
⊢ P&Q ∈ fun f => ¬~f ∈ Γ
Tactic:
case adj P Q prf₁ prf₂ ih₁ ih₂ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
  have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
  cases l₃
  case inl left => exact l₁ left
  case inr right => exact l₂ right
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ
Tactic:
assumption
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
⊢ Q ∈ fun f => ¬~f ∈ Γ
Tactic:
intros h₄
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
⊢ False
Tactic:
have l₁ := ih₁ ⟨prf₂⟩
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
⊢ False
Tactic:
have prf₂ := BProof.mp (BProof.ax h₄) thm₂
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂✝ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
prf₂ : BProof Γ ~P
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂✝ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
prf₂ : BProof Γ ~P
⊢ False
Tactic:
exact l₁ (h₁.mpr ⟨prf₂⟩)
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
⊢ P&Q ∈ fun f => ¬~f ∈ Γ
Tactic:
intros h₄
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
⊢ False
Tactic:
have l₁ := ih₁ ⟨prf₁⟩
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have l₂ := ih₂ ⟨prf₂⟩
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
⊢ False
Tactic:
have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
State after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
l₃ : ~P ∈ Γ ∨ ~Q ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
l₃ : ~P ∈ Γ ∨ ~Q ∈ Γ
⊢ False
Tactic:
cases l₃
State after:
case inl
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
h✝ : ~P ∈ Γ
⊢ False

case inr
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
h✝ : ~Q ∈ Γ
⊢ False

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
left : ~P ∈ Γ
⊢ False
Tactic:
case inl left => exact l₁ left
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
right : ~Q ∈ Γ
⊢ False
Tactic:
case inr right => exact l₂ right
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
left : ~P ∈ Γ
⊢ False
Tactic:
exact l₁ left
State after:
no goals

State before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
right : ~Q ∈ Γ
⊢ False
Tactic:
exact l₂ right
State after:
no goals