Theorem: truthLemma
Proof state before:
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
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ plus (□P) X ∧ minus (□P) X ∧ oh (□P) X
Tactic:
repeat' constructor
Proof state after:
case left
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
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ plus (□P) X

case right.left
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
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ minus (□P) X

case right.right
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
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ oh (□P) X