have ⟨M,⟨i,ii,iii,iv⟩⟩ := MG
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P