internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]
Tactic:
use Fs, δ
Proof state after:
case h
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (Fs, δ) ∈ H β ∧ (if δ = [] then [] else [(Fs, δ ++ [∗β])]) = [(Fs, δ ++ [∗β])]
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (Fs, δ) ∈ H β ∧ (if δ = [] then [] else [(Fs, δ ++ [∗β])]) = [(Fs, δ ++ [∗β])]
Tactic:
simp_all
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (Con (Yset (Fs, δ ++ [∗β]) ψ))
Tactic:
simp [conEval, Yset]
Proof state after:
case h.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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ ++ [∗β]⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ ++ [∗β]⌉⌉ψ) → evaluate M w f
Tactic:
intro f f_in
Proof state after:
case h.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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w f
Tactic:
cases f_in
Proof state after:
case h.right.inl
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M w f

case h.right.inr
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
h✝ : f = (~⌈⌈δ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_in_F : f ∈ Fs
⊢ evaluate M w f
Tactic:
case inl f_in_F => exact repl_w_.2 f f_in_F
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_def : f = (~⌈⌈δ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w f
Tactic:
case inr f_def =>
  subst f_def
  simp [boxes_append,evalBoxes]
  have v_notStarβψ := right_to_left_claim W M v v_ρ
  exact ⟨v, ⟨w_ρ_v, v_notStarβψ⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_in_F : f ∈ Fs
⊢ evaluate M w f
Tactic:
exact repl_w_.2 f f_in_F
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
f : Formula
f_def : f = (~⌈⌈δ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w f
Tactic:
subst f_def
Proof state after:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (~⌈⌈δ ++ [∗β]⌉⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (~⌈⌈δ ++ [∗β]⌉⌉ψ)
Tactic:
simp [boxes_append,evalBoxes]
Proof state after:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ x, relateSeq M δ w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ x, relateSeq M δ w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
Tactic:
have v_notStarβψ := right_to_left_claim W M v v_ρ
Proof state after:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
v_notStarβψ : ∃ x, Relation.ReflTransGen (relate M β) v x ∧ ¬evaluate M x ψ
⊢ ∃ x, relateSeq M δ w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
Theorem: localDiamondTruth
Proof state before:
ψ : 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
Fs : List Formula
δ : List Program
v : W
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 β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
v_notStarβψ : ∃ x, Relation.ReflTransGen (relate M β) v x ∧ ¬evaluate M x ψ
⊢ ∃ x, relateSeq M δ w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
Tactic:
exact ⟨v, ⟨w_ρ_v, v_notStarβψ⟩⟩
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
⊢ evaluate M w (~ψ) → evaluate M w ρ
Tactic:
intro w_nPsi
Proof state after:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
w_nPsi : evaluate M w (~ψ)
⊢ evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
w_nPsi : evaluate M w (~ψ)
⊢ evaluate M w ρ
Tactic:
unfold_let ρ
Proof state after:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
w_nPsi : evaluate M w (~ψ)
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
w_nPsi : evaluate M w (~ψ)
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
rw [disEval, helper]
Proof state after:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ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
w_nPsi : evaluate M w (~ψ)
⊢ ∃ Fδ ∈ H (∗β), evaluate M w (Con (Yset Fδ ψ))