Theorem: lindenbaumAvoids
Proof state before:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head : Form
tail : List Form
l₆ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
head' : Form
tail' : List Form
l₇ : { x | x ∈ head' :: tail' } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head' :: tail')¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
prf₆ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
prf₇ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head' tail')
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head' tail')
prf₈ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j + 0)).fst&Form.conjoinList head' tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((((Denumerable.ofNat (Form × Form)
              (j +
                0)).fst&Form.conjoinList head'
            tail')&Form.conjoinList head tail)¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False
Tactic:
have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
Proof state after:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head : Form
tail : List Form
l₆ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
head' : Form
tail' : List Form
l₇ : { x | x ∈ head' :: tail' } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head' :: tail')¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
prf₆ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
prf₇ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head' tail')
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head' tail')
prf₈ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j + 0)).fst&Form.conjoinList head' tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((((Denumerable.ofNat (Form × Form)
              (j +
                0)).fst&Form.conjoinList head'
            tail')&Form.conjoinList head tail)¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
prf₉ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False