Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notAndSplit : (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
cases' notAndSplit with notQ_in_X notR_in_X
Proof state after:
case intro.intro.intro.intro.intro.right.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R

case intro.intro.intro.intro.intro.right.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R