Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
X_β_Z : relate (↑MG) β YS.head Z
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ ∃ ys, Z = ys.head ∧ YS.last = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
Tactic:
refine ⟨YS.tail, ?_, ?_, ?_⟩
Proof state after:
case refine_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
X_β_Z : relate (↑MG) β YS.head Z
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ Z = YS.tail.head

case refine_2
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
X_β_Z : relate (↑MG) β YS.head Z
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.last = YS.tail.last

case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
X_β_Z : relate (↑MG) β YS.head Z
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ ∀ (i : Fin m), relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)