Theorem: guardToStarDiamond (Pdl/Unfold.lean)

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
⊢ (~⌈∗β⌉ψ)⊨ρ
Tactic:
intro W M
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
have claim : ∀ u v, (M,v) ⊨ ρ → relate M β u v → (M,u) ⊨ ρ := by
  intro u v v_rho u_β_v
  have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
    simp [modelCanSemImplyForm] at *
    use v
  have u_2 : (M, u) ⊨ (ρ ⋀ repl_in_F x ρ σ0) ⋁ (repl_in_F x ρ σ1) := by
    have repl_equiv := repl_in_F_equiv x ρ beta_equiv
    simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
    have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
    rw [nox] at repl_equiv
    rw [equiv_iff _ _ repl_equiv] at u_
    simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
    tauto
  simp only [modelCanSemImplyForm, Formula.or, evaluatePoint, evaluate] at u_2
  rw [← @or_iff_not_and_not] at u_2
  specialize repl_imp_rho W M u
  aesop
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
intro w hyp
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ
⊢ ∀ ψ ∈ [ρ], evaluate M w ψ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ
⊢ ∀ ψ ∈ [ρ], evaluate M w ψ
Tactic:
simp only [Formula.or, List.mem_singleton, forall_eq, evaluate, relate, not_forall, exists_prop] at *
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
⊢ evaluate M w ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w : W
hyp : ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
⊢ evaluate M w ρ
Tactic:
rcases hyp with ⟨v, w_bS_v, v_Psi⟩
State after:
case intro.intro
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
v_Psi : ¬evaluate M v ψ
⊢ evaluate M w ρ

State before:
case intro.intro
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
v_Psi : ¬evaluate M v ψ
⊢ evaluate M w ρ
Tactic:
induction w_bS_v using Relation.ReflTransGen.head_induction_on
State after:
case intro.intro.refl
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ

case intro.intro.head
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
a✝¹ c✝ : W
h'✝ : relate M β a✝¹ c✝
h✝ : Relation.ReflTransGen (relate M β) c✝ v
a✝ : evaluate M c✝ ρ
⊢ evaluate M a✝¹ ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ
Tactic:
case refl =>
  specialize notPsi_imp_rho W M v
  simp_all
State after:
no goals

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
⊢ evaluate M u1 ρ
Tactic:
case head u1 u2 u1_b_u2 _ IH =>
  specialize claim u1 u2
  specialize notPsi_imp_rho W M u1
  simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
  simp_all
State after:
no goals

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
⊢ ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
Tactic:
intro u v v_rho u_β_v
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨ρ
Tactic:
have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
  simp [modelCanSemImplyForm] at *
  use v
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ
Tactic:
have u_2 : (M, u) ⊨ (ρ ⋀ repl_in_F x ρ σ0) ⋁ (repl_in_F x ρ σ1) := by
  have repl_equiv := repl_in_F_equiv x ρ beta_equiv
  simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
  have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
  rw [nox] at repl_equiv
  rw [equiv_iff _ _ repl_equiv] at u_
  simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
  tauto
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
⊢ (M, u)⊨ρ
Tactic:
simp only [modelCanSemImplyForm, Formula.or, evaluatePoint, evaluate] at u_2
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : ¬(¬(evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0)) ∧ ¬evaluate M u (repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : ¬(¬(evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0)) ∧ ¬evaluate M u (repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ
Tactic:
rw [← @or_iff_not_and_not] at u_2
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
⊢ (M, u)⊨ρ
Tactic:
specialize repl_imp_rho W M u
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
repl_imp_rho : (∀ φ ∈ [repl_in_F x ρ σ1], evaluate M u φ) → ∀ ψ ∈ [ρ], evaluate M u ψ
⊢ (M, u)⊨ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : evaluate M u ρ ∧ evaluate M u (repl_in_F x ρ σ0) ∨ evaluate M u (repl_in_F x ρ σ1)
repl_imp_rho : (∀ φ ∈ [repl_in_F x ρ σ1], evaluate M u φ) → ∀ ψ ∈ [ρ], evaluate M u ψ
⊢ (M, u)⊨ρ
Tactic:
aesop
State after:
no goals

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
⊢ (M, u)⊨(~⌈β⌉~ρ)
Tactic:
simp [modelCanSemImplyForm] at *
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
⊢ ∃ x, relate M β u x ∧ evaluate M x ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
⊢ ∃ x, relate M β u x ∧ evaluate M x ρ
Tactic:
use v
State after:
no goals

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
have repl_equiv := 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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : repl_in_F x ρ (~⌈β⌉~·x)≡repl_in_F x ρ ((·x)⋀σ0⋁σ1)
⊢ (M, u)⊨ρ⋀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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : repl_in_F x ρ (~⌈β⌉~·x)≡repl_in_F x ρ ((·x)⋀σ0⋁σ1)
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ⋀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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈repl_in_P x ρ β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
rw [nox] at repl_equiv
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
rw [equiv_iff _ _ repl_equiv] at u_
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀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
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
Tactic:
simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ψ → evaluate M w ρ
u_ : (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
⊢ (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ψ → evaluate M w ρ
u_ : (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
⊢ (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
Tactic:
tauto
State after:
no goals

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ
Tactic:
specialize notPsi_imp_rho W M v
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M v φ) → ∀ ψ ∈ [ρ], evaluate M v ψ
⊢ evaluate M v ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M v φ) → ∀ ψ ∈ [ρ], evaluate M v ψ
⊢ evaluate M v ρ
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))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
⊢ evaluate M u1 ρ
Tactic:
specialize claim u1 u2
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
⊢ evaluate M u1 ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
⊢ evaluate M u1 ρ
Tactic:
specialize notPsi_imp_rho W M u1
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M u1 φ) → ∀ ψ ∈ [ρ], evaluate M u1 ψ
⊢ evaluate M u1 ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : (M, u2)⊨ρ → relate M β u1 u2 → (M, u1)⊨ρ
notPsi_imp_rho : (∀ φ ∈ [~ψ], evaluate M u1 φ) → ∀ ψ ∈ [ρ], evaluate M u1 ψ
⊢ evaluate M u1 ρ
Tactic:
simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
State after:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : evaluate M u2 ρ → relate M β u1 u2 → evaluate M u1 ρ
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ¬evaluate M u1 ψ → evaluate M u1 ρ
⊢ evaluate M u1 ρ

State before:
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
w v : W
v_Psi : ¬evaluate M v ψ
u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ
claim : evaluate M u2 ρ → relate M β u1 u2 → evaluate M u1 ρ
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ¬evaluate M u1 ψ → evaluate M u1 ρ
⊢ evaluate M u1 ρ
Tactic:
simp_all
State after:
no goals