Theorem: localDiamondTruth
Proof state before:
case a.inr.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x) = ⌈⌈Fδ.2⌉⌉~ρ) ∧ List.map (repl_in_F x ρ) Fδ.1 = Fδ.1
Tactic:
constructor
Proof state after:
case a.inr.a.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ repl_in_F x ρ (⌈⌈Fδ.2⌉⌉~·x) = ⌈⌈Fδ.2⌉⌉~ρ

case a.inr.a.right
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fδ : List Formula × List Program
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ List.map (repl_in_F x ρ) Fδ.1 = Fδ.1