Theorem: lindenbaumAvoids (Fine/SystemB/Lindenbaum.lean)

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
have l₁ := formalFixed t.property
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
rw [←l₁] at h₁
State after:
t : Th
Δ : Ctx
h₁ : ▲↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅

State before:
t : Th
Δ : Ctx
h₁ : ▲↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
exact h₁
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲lindenbaumSequence t Δ (i + 1, 0) ∩ Δ = ∅
Tactic:
change
  ▲{ f : Form | ∃j : Nat, f ∈ lindenbaumSequence t Δ ⟨i, j⟩ } ∩ Δ = ∅
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ = ∅

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ¬Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ¬Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
Tactic:
intros h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
⊢ False
Tactic:
have ⟨w,⟨prf₁⟩,l₁⟩ := h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Tactic:
clear h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Tactic:
have ⟨s,l₂,prf₂⟩ := BProof.compactness prf₁
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
⊢ False
Tactic:
have ⟨j, l₃⟩ := finiteExhaustion lindenbaumStageMonotone l₂
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ False
Tactic:
have l₄ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
have prf₃ := BProof.monotone l₃ prf₂
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
⊢ False
Tactic:
have l₅ := Set.not_nonempty_iff_eq_empty.mpr l₄
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
l₅ : ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j) ∩ Δ)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
l₅ : ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j) ∩ Δ)
⊢ False
Tactic:
exact l₅ ⟨w, ⟨⟨prf₃⟩,l₁⟩⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
Tactic:
intros h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
⊢ False
Tactic:
have ⟨w₁,l₁,l₂⟩ := h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 1)
l₂ : w₁ ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 1)
l₂ : w₁ ∈ Δ
⊢ False
Tactic:
unfold lindenbaumSequence at l₁
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲match (i, j + 1) with
      | (0, 0) => ↑t
      | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
      | (i, Nat.succ j) =>
        let prev := lindenbaumSequence t Δ (i, j);
        let l := (Denumerable.ofNat (Form × Form) j).fst;
        let r := (Denumerable.ofNat (Form × Form) j).snd;
        if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲match (i, j + 1) with
      | (0, 0) => ↑t
      | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
      | (i, Nat.succ j) =>
        let prev := lindenbaumSequence t Δ (i, j);
        let l := (Denumerable.ofNat (Form × Form) j).fst;
        let r := (Denumerable.ofNat (Form × Form) j).snd;
        if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
split at l₁
State after:
case h_1
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
heq✝ : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False

case h_2
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq✝ : (i, j + 1) = (Nat.succ i✝, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
⊢ False

case h_3
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ j✝ : ℕ
heq✝ : (i, j + 1) = (i✝, Nat.succ j✝)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i✝, j✝);
      let l := (Denumerable.ofNat (Form × Form) j✝).fst;
      let r := (Denumerable.ofNat (Form × Form) j✝).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
heq : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False
Tactic:
case h_1 x heq => injection heq with heq; contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
heq : (i, j + 1) = (Nat.succ x, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
⊢ False
Tactic:
case h_2 x heq => injection heq with heq; contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
case h_3 x n m heq =>
  have l₃ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
  injection heq with heq₁ heq₂
  injection heq₂ with heq₂
  rw [←heq₁,←heq₂] at l₁
  clear n m x heq₁ heq₂ h₃
  dsimp at l₁ j
  split at l₁
  case inr h₄ => exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
  case inl h₄ =>
    split at l₁
    case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
    case inr h₅ =>
      have ⟨prf₁⟩ := l₁
      have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
      have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
      clear l₁ l₂ l₄ h₅
      have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
      have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
      have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
      have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
      have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
      have ⟨prf₅⟩ := h₄
      clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
      cases lst₁
      all_goals 
        cases lst₂
      case' nil.nil =>
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' nil.cons head tail =>
        have := BProof.proveList l₇
        have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
        have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' cons.nil head tail => 
        have := BProof.proveList l₆
        have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
        have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' cons.cons head tail head' tail'=> 
        have prf₆ := BProof.proveList l₆
        have prf₇ := BProof.proveList l₇
        have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
        have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
        have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
        have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
heq : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False
Tactic:
injection heq with heq
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
l₁ : w₁ ∈ ▲↑t
heq : i = 0
snd_eq✝ : j + 1 = 0
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
l₁ : w₁ ∈ ▲↑t
heq : i = 0
snd_eq✝ : j + 1 = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
heq : (i, j + 1) = (Nat.succ x, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
⊢ False
Tactic:
injection heq with heq
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
heq : i = Nat.succ x
snd_eq✝ : j + 1 = 0
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
heq : i = Nat.succ x
snd_eq✝ : j + 1 = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
have l₃ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
injection heq with heq₁ heq₂
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : j + 1 = Nat.succ m
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : j + 1 = Nat.succ m
⊢ False
Tactic:
injection heq₂ with heq₂
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False
Tactic:
rw [←heq₁,←heq₂] at l₁
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False
Tactic:
clear n m x heq₁ heq₂ h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
dsimp at l₁ j
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲if
          (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
            ▲lindenbaumSequence t Δ (i, j + 0) then
        if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
          lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
        else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
      else lindenbaumSequence t Δ (i, j + 0)
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲if
          (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
            ▲lindenbaumSequence t Δ (i, j + 0) then
        if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
          lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
        else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
      else lindenbaumSequence t Δ (i, j + 0)
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
split at l₁
State after:
case inl
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h✝ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False

case inr
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h✝ :
  ¬(Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
      ▲lindenbaumSequence t Δ (i, j + 0)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  ¬(Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
      ▲lindenbaumSequence t Δ (i, j + 0)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False
Tactic:
case inr h₄ => exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False
Tactic:
case inl h₄ =>
  split at l₁
  case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
  case inr h₅ =>
    have ⟨prf₁⟩ := l₁
    have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
    have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
    clear l₁ l₂ l₄ h₅
    have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
    have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
    have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
    have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
    have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
    have ⟨prf₅⟩ := h₄
    clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
    cases lst₁
    all_goals 
      cases lst₂
    case' nil.nil =>
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' nil.cons head tail =>
      have := BProof.proveList l₇
      have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
      have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' cons.nil head tail => 
      have := BProof.proveList l₆
      have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
      have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' cons.cons head tail head' tail'=> 
      have prf₆ := BProof.proveList l₆
      have prf₇ := BProof.proveList l₇
      have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
      have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
      have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
      have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  ¬(Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
      ▲lindenbaumSequence t Δ (i, j + 0)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False
Tactic:
split at l₁
State after:
case inl
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h✝ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False

case inr
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h✝ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False
Tactic:
case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
⊢ False
Tactic:
case inr h₅ =>
  have ⟨prf₁⟩ := l₁
  have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
  have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
  clear l₁ l₂ l₄ h₅
  have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
  have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
  have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
  have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
  have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
  have ⟨prf₅⟩ := h₄
  clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
  cases lst₁
  all_goals 
    cases lst₂
  case' nil.nil =>
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
  case' nil.cons head tail =>
    have := BProof.proveList l₇
    have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
    have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
  case' cons.nil head tail => 
    have := BProof.proveList l₆
    have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
    have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
  case' cons.cons head tail head' tail'=> 
    have prf₆ := BProof.proveList l₆
    have prf₇ := BProof.proveList l₇
    have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
    have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
    have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
    have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
⊢ False
Tactic:
have ⟨prf₁⟩ := l₁
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
⊢ False
Tactic:
have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₄ : w₂ ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₄ : w₂ ∈ Δ
⊢ False
Tactic:
have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₄ : w₂ ∈ Δ
l₅ : w₁¦w₂ ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₄ : w₂ ∈ Δ
l₅ : w₁¦w₂ ∈ Δ
⊢ False
Tactic:
clear l₁ l₂ l₄ h₅
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
⊢ False
Tactic:
have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
⊢ False
Tactic:
have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
⊢ False
Tactic:
have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Tactic:
have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
⊢ False
Tactic:
have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Tactic:
have ⟨prf₅⟩ := h₄
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Tactic:
clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Tactic:
cases lst₁
State after:
case nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False

case cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
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)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

State before:
case nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False

case cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
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)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False
Tactic:
all_goals 
  cases lst₂
State after:
case nil.nil
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)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False

case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
⊢ False

case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False

State before:
case nil.nil
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)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False

case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
⊢ False

case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False
Tactic:
case' nil.nil =>
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
⊢ False

case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
⊢ False

case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False
Tactic:
case' nil.cons head tail =>
  have := BProof.proveList l₇
  have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
  have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False
Tactic:
case' cons.nil head tail => 
  have := BProof.proveList l₆
  have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
  have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
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₂)
⊢ False

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₂)
⊢ False
Tactic:
case' cons.cons head tail head' tail'=> 
  have prf₆ := BProof.proveList l₆
  have prf₇ := BProof.proveList l₇
  have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
  have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
  have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
  have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
case cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
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)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False
Tactic:
cases lst₂
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

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₂)
⊢ False

State before:
case nil.nil
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)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False
Tactic:
have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
State after:
case nil.nil
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)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False

State before:
case nil.nil
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)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
⊢ False
Tactic:
have := BProof.proveList l₇
State after:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
State after:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝ : 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)
⊢ False

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝ : 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)
⊢ False
Tactic:
have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
State after:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝¹ : 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)
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)
⊢ False

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝¹ : 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)
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)
⊢ False
Tactic:
have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
State after:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝² : 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)
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)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False

State before:
case nil.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)
l₆ : { x | x ∈ [] } ⊆ 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 []⊃w₁¦w₂)
this✝² : 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)
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)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
⊢ False
Tactic:
have := BProof.proveList l₆
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝ : 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)
⊢ False

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝ : 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)
⊢ False
Tactic:
have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝¹ : 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)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form)
          (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝¹ : 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)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form)
          (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False
Tactic:
have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
State after:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝² : 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)
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form)
          (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False

State before:
case cons.nil
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)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
this✝² : 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)
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form)
          (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals

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₂)
⊢ False
Tactic:
have prf₆ := BProof.proveList l₆
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)
⊢ False

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)
⊢ False
Tactic:
have prf₇ := BProof.proveList l₇
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')
⊢ False

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')
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
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')
⊢ False

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')
⊢ False
Tactic:
have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
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)
⊢ False

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)
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
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)
⊢ False

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)
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

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)
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
Tactic:
have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
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)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False

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)
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)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
State after:
no goals