Theorem: truthLemma
Proof state before:
case bottom
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
⊢ ∀ (X : ↑Worlds), plus bottom X ∧ minus bottom X ∧ oh bottom X

case atom_prop
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Char
⊢ ∀ (X : ↑Worlds), plus (·a✝) X ∧ minus (·a✝) X ∧ oh (·a✝) X

case neg
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Formula
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
⊢ ∀ (X : ↑Worlds), plus (~a✝) X ∧ minus (~a✝) X ∧ oh (~a✝) X

case And
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (X : ↑Worlds), plus a✝¹ X ∧ minus a✝¹ X ∧ oh a✝¹ X
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
⊢ ∀ (X : ↑Worlds), plus (a✝¹⋀a✝) X ∧ minus (a✝¹⋀a✝) X ∧ oh (a✝¹⋀a✝) X

case box
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Formula
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
⊢ ∀ (X : ↑Worlds), plus (□a✝) X ∧ minus (□a✝) X ∧ oh (□a✝) X
Tactic:
all_goals intro X
Proof state after:
case bottom
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
X : ↑Worlds
⊢ plus bottom X ∧ minus bottom X ∧ oh bottom X

case atom_prop
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Char
X : ↑Worlds
⊢ plus (·a✝) X ∧ minus (·a✝) X ∧ oh (·a✝) X

case neg
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Formula
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
X : ↑Worlds
⊢ plus (~a✝) X ∧ minus (~a✝) X ∧ oh (~a✝) X

case And
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (X : ↑Worlds), plus a✝¹ X ∧ minus a✝¹ X ∧ oh a✝¹ X
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
X : ↑Worlds
⊢ plus (a✝¹⋀a✝) X ∧ minus (a✝¹⋀a✝) X ∧ oh (a✝¹⋀a✝) X

case box
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
a✝ : Formula
a_ih✝ : ∀ (X : ↑Worlds), plus a✝ X ∧ minus a✝ X ∧ oh a✝ X
X : ↑Worlds
⊢ plus (□a✝) X ∧ minus (□a✝) X ∧ oh (□a✝) X