Theorem: guardToStar (Pdl/Unfold.lean)

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)⊨ρ
⊢ ρ⊨⌈∗β⌉ψ
Tactic:
intro W M w
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 : W
⊢ (∀ φ ∈ [ρ], evaluate M w φ) → ∀ ψ_1 ∈ [⌈∗β⌉ψ], evaluate M w ψ_1

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 : W
⊢ (∀ φ ∈ [ρ], evaluate M w φ) → ∀ ψ_1 ∈ [⌈∗β⌉ψ], evaluate M w ψ_1
Tactic:
simp only [List.mem_singleton, forall_eq, evaluate, relate]
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 : W
⊢ evaluate M w ρ → ∀ (v : W), Relation.ReflTransGen (relate M β) w v → evaluate M v ψ

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 : W
⊢ evaluate M w ρ → ∀ (v : W), Relation.ReflTransGen (relate M β) w v → evaluate M v ψ
Tactic:
intro w_rho v w_bS_v
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 : W
w_rho : evaluate M w ρ
v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
⊢ evaluate M v ψ

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 : W
w_rho : evaluate M w ρ
v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
⊢ evaluate M v ψ
Tactic:
induction w_bS_v using Relation.ReflTransGen.head_induction_on
State after:
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 ψ

case head
β : 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 a✝¹ c✝ : W
h'✝ : relate M β a✝¹ c✝
h✝ : Relation.ReflTransGen (relate M β) c✝ v
a✝ : evaluate M c✝ ρ → evaluate M v ψ
w_rho : evaluate M a✝¹ ρ
⊢ evaluate M v ψ

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:
case head u1 u2 u1_b_u2 _ IH =>
  apply IH
  exact fortysix W M u1 u2 w_rho u1_b_u2
State after:
no goals

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), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
Tactic:
intro W M w v w_rho w_β_v
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
⊢ (M, v)⊨ρ

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
this : (M, w)⊨⌈β⌉ρ
⊢ (M, v)⊨ρ
Tactic:
simp [evaluate,relate,modelCanSemImplyForm] at this
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
this : ∀ (v : W), relate M β w v → evaluate M v ρ
⊢ (M, v)⊨ρ

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
this : ∀ (v : W), relate M β w v → evaluate M v ρ
⊢ (M, v)⊨ρ
Tactic:
exact this v w_β_v
State after:
no goals

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)⊨⌈β⌉ρ
Tactic:
have by_ass : (M,w) ⊨ (repl_in_F x ρ) (χ0 ⋁ χ1) := by apply rho_imp_repl; simp; exact w_rho; simp
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)⊨⌈β⌉ρ

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)
⊢ (M, w)⊨⌈β⌉ρ
Tactic:
have := repl_in_F_equiv x ρ beta_equiv
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 ρ (⌈β⌉·x)≡repl_in_F x ρ ((·x)⋀χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ

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
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)⊨⌈β⌉ρ

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
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)⊨⌈β⌉ρ

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
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)⊨⌈β⌉ρ

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]
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))

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
State after:
no goals

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
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)]

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
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)]

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
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)]

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
State after:
no goals

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
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)⊨ρ

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
State after:
no goals

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 *
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)

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
State after:
no goals

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
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 ρ
⊢ ψ ∈ [ψ]

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
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 ρ
⊢ ψ ∈ [ψ]

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
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 ρ
⊢ ψ ∈ [ψ]

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
State after:
no goals

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
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 ρ

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
State after:
no goals