internlm/Lean-Github huggingface dataset:
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : repl_in_F x ρ (⌈β⌉·x)≡repl_in_F x ρ ((·x)⋀χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at this
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈repl_in_P x ρ β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
⊢ (M, w)⊨⌈β⌉ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈repl_in_P x ρ β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈repl_in_P x ρ β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨⌈β⌉ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈repl_in_P x ρ β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
rw [nox] at this
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨⌈β⌉ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
rw [equiv_iff _ _ this]
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
this✝ : (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
this : (⌈β⌉ρ)≡(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
nox : repl_in_P x ρ β = β
⊢ (M, w)⊨(~(~ρ⋀repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
Tactic:
simp_all
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
Tactic:
apply rho_imp_repl
Proof state after:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ ∀ φ ∈ [ρ], evaluate M w φ

case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Theorem: guardToStar
Proof state before:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ ∀ φ ∈ [ρ], evaluate M w φ

case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Tactic:
simp
Proof state after:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ evaluate M w ρ

case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Theorem: guardToStar
Proof state before:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ evaluate M w ρ

case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Tactic:
exact w_rho
Proof state after:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Theorem: guardToStar
Proof state before:
case a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ repl_in_F x ρ (χ0⋁χ1) ∈ [repl_in_F x ρ (χ0⋁χ1)]
Tactic:
simp
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
⊢ (M, w)⊨repl_in_F x ρ (·x)
Tactic:
simp
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
⊢ (M, w)⊨ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
⊢ (M, w)⊨ρ
Tactic:
exact w_rho
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
obvious : (M, w)⊨repl_in_F x ρ (·x)
⊢ (M, w)⊨repl_in_F x ρ ((·x)⋀χ0⋁χ1)
Tactic:
simp [evaluate,relate,modelCanSemImplyForm] at *
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(~(~(·x)⋀χ0)⋀(~χ1))
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M w ρ
w_β_v : relate M β w v
rho_imp_repl : ρ⊨(~(~repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
by_ass : ¬evaluate M w (repl_in_F x ρ χ0) → evaluate M w (repl_in_F x ρ χ1)
obvious : evaluate M w ρ
⊢ (evaluate M w ρ → ¬evaluate M w (repl_in_F x ρ χ0)) → evaluate M w (repl_in_F x ρ χ1)
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(~(~(·x)⋀χ0)⋀(~χ1))
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M w ρ
w_β_v : relate M β w v
rho_imp_repl : ρ⊨(~(~repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
by_ass : ¬evaluate M w (repl_in_F x ρ χ0) → evaluate M w (repl_in_F x ρ χ1)
obvious : evaluate M w ρ
⊢ (evaluate M w ρ → ¬evaluate M w (repl_in_F x ρ χ0)) → evaluate M w (repl_in_F x ρ χ1)
Tactic:
tauto
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
case refl
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ evaluate M v ψ
Tactic:
apply rho_imp_psi
Proof state after:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ∀ φ ∈ [ρ], evaluate M v φ

case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Theorem: guardToStar
Proof state before:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ∀ φ ∈ [ρ], evaluate M v φ

case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Tactic:
simp
Proof state after:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ evaluate M v ρ

case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Theorem: guardToStar
Proof state before:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ evaluate M v ρ

case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Tactic:
assumption
Proof state after:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Theorem: guardToStar
Proof state before:
case refl.a
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M v ρ
⊢ ψ ∈ [ψ]
Tactic:
simp
Proof state after:
no goals
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ → evaluate M v ψ
w_rho : evaluate M u1 ρ
⊢ evaluate M v ψ
Tactic:
apply IH
Proof state after:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ → evaluate M v ψ
w_rho : evaluate M u1 ρ
⊢ evaluate M u2 ρ
Theorem: guardToStar
Proof state before:
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ → evaluate M v ψ
w_rho : evaluate M u1 ρ
⊢ evaluate M u2 ρ
Tactic:
exact fortysix W M u1 u2 w_rho u1_b_u2
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
γ : Program
ψ : Formula
ℓ : TP γ
⊢ (⌈γ⌉ψ)⋀signature γ ℓ≡Con (Xset γ ℓ ψ)⋀signature γ ℓ
Tactic:
cases γ
Proof state after:
case atom_prog
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ

case sequence
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ

case union
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ

case star
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ

case test
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ
Tactic:
case atom_prog =>
  sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ
Tactic:
case test =>
  sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ
Tactic:
case union =>
  sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ
Tactic:
case sequence =>
  sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ
Tactic:
case star =>
  sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth'
Proof state before:
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth
Proof state before:
γ : Program
ψ : Formula
⊢ (⌈γ⌉ψ)≡dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))
Tactic:
intro W M w
Proof state after:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Theorem: localBoxTruth
Proof state before:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
constructor
Proof state after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) → evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))

case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))) → evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) → evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
intro w_γψ
Proof state after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Theorem: localBoxTruth
Proof state before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
rw [disEval]
Proof state after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
Theorem: localBoxTruth
Proof state before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
Tactic:
sorry
Proof state after:
no goals
Theorem: localBoxTruth
Proof state before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))) → evaluate M w (⌈γ⌉ψ)
Tactic:
intro w_Cons
Proof state after:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rw [disEval] at w_Cons
Proof state after:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rcases w_Cons with ⟨φ, φ_in, w_φ⟩
Proof state after:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
φ_in : φ ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)
w_φ : evaluate M w φ
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
φ_in : φ ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)
w_φ : evaluate M w φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
simp at φ_in
Proof state after:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
φ_in : ∃ a ∈ allTP γ, Con (Xset γ a ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
φ_in : ∃ a ∈ allTP γ, Con (Xset γ a ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rcases φ_in with ⟨ℓ, ℓ_in, def_φ⟩
Proof state after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
def_φ : Con (Xset γ ℓ ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
def_φ : Con (Xset γ ℓ ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
subst def_φ
Proof state after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : evaluate M w (Con (Xset γ ℓ ψ))
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : evaluate M w (Con (Xset γ ℓ ψ))
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rw [conEval] at w_φ
Proof state after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
have := localBoxTruth' γ ψ ℓ W M w
Proof state after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
this : evaluate M w ((⌈γ⌉ψ)⋀signature γ ℓ) ↔ evaluate M w (Con (Xset γ ℓ ψ)⋀signature γ ℓ)
⊢ evaluate M w (⌈γ⌉ψ)