cases P
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
case bottom
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)

case atom_prop
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : ℕ
⊢ ((·a✝) ∈ ↑X → evaluate (↑MG) X (·a✝)) ∧ ((~·a✝) ∈ ↑X → ¬evaluate (↑MG) X (·a✝))

case neg
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : Formula
⊢ ((~a✝) ∈ ↑X → evaluate (↑MG) X (~a✝)) ∧ ((~~a✝) ∈ ↑X → ¬evaluate (↑MG) X (~a✝))

case and
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ a✝ : Formula
⊢ (a✝¹⋀a✝ ∈ ↑X → evaluate (↑MG) X (a✝¹⋀a✝)) ∧ ((~a✝¹⋀a✝) ∈ ↑X → ¬evaluate (↑MG) X (a✝¹⋀a✝))

case box
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ : Program
a✝ : Formula
⊢ ((⌈a✝¹⌉a✝) ∈ ↑X → evaluate (↑MG) X (⌈a✝¹⌉a✝)) ∧ ((~⌈a✝¹⌉a✝) ∈ ↑X → ¬evaluate (↑MG) X (⌈a✝¹⌉a✝))