Theorem: existsBoxFP (Pdl/Unfold.lean)

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
γ : Program
v_γ_w : relate M γ v w
ℓ : TP γ
v_conF : (M, v)⊨Con (F γ ℓ)
⊢ ∃ δ ∈ P γ ℓ, relateSeq M δ v w
Tactic:
cases γ
State after:
case atom_prog
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
ℓ : TP (·a✝)
v_conF : (M, v)⊨Con (F (·a✝) ℓ)
⊢ ∃ δ ∈ P (·a✝) ℓ, relateSeq M δ v w

case sequence
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹;'a✝) v w
ℓ : TP (a✝¹;'a✝)
v_conF : (M, v)⊨Con (F (a✝¹;'a✝) ℓ)
⊢ ∃ δ ∈ P (a✝¹;'a✝) ℓ, relateSeq M δ v w

case union
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹⋓a✝) v w
ℓ : TP (a✝¹⋓a✝)
v_conF : (M, v)⊨Con (F (a✝¹⋓a✝) ℓ)
⊢ ∃ δ ∈ P (a✝¹⋓a✝) ℓ, relateSeq M δ v w

case star
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Program
v_γ_w : relate M (∗a✝) v w
ℓ : TP (∗a✝)
v_conF : (M, v)⊨Con (F (∗a✝) ℓ)
⊢ ∃ δ ∈ P (∗a✝) ℓ, relateSeq M δ v w

case test
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Formula
v_γ_w : relate M (?'a✝) v w
ℓ : TP (?'a✝)
v_conF : (M, v)⊨Con (F (?'a✝) ℓ)
⊢ ∃ δ ∈ P (?'a✝) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
ℓ : TP (·a✝)
v_conF : (M, v)⊨Con (F (·a✝) ℓ)
⊢ ∃ δ ∈ P (·a✝) ℓ, relateSeq M δ v w
Tactic:
case atom_prog =>
  simp [F, P, relateSeq] at *
  exact v_γ_w
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
case test τ =>
  simp only [relate] at v_γ_w
  rcases v_γ_w with ⟨v_is_w, v_τ⟩
  cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩ )
  all_goals
    simp_all [modelCanSemImplyForm, evaluatePoint, F, P, relateSeq, TP, testsOfProgram]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
case union α β =>
  simp at v_γ_w
  cases v_γ_w
  case inl v_α_w =>
    have v_Fℓα : evaluate M v (Con (F α ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
    have IHα := existsBoxFP α v_α_w ℓ v_Fℓα rcases IHα with ⟨δ, _⟩
    use δ
    simp_all [P]
  case inr v_β_w =>
    have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
    have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ rcases IHβ with ⟨δ, _⟩
    use δ
    simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
ℓ : TP (·a✝)
v_conF : (M, v)⊨Con (F (·a✝) ℓ)
⊢ ∃ δ ∈ P (·a✝) ℓ, relateSeq M δ v w
Tactic:
simp [F, P, relateSeq] at *
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
ℓ : TP (·a✝)
v_γ_w : M.Rel a✝ v w
v_conF : (M, v)⊨(~Formula.bottom)
⊢ M.Rel a✝ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
ℓ : TP (·a✝)
v_γ_w : M.Rel a✝ v w
v_conF : (M, v)⊨(~Formula.bottom)
⊢ M.Rel a✝ v w
Tactic:
exact v_γ_w
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
simp only [relate] at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_γ_w : v = w ∧ evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_γ_w : v = w ∧ evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
rcases v_γ_w with ⟨v_is_w, v_τ⟩
State after:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w

State before:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩ )
State after:
case intro.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w

case intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w

State before:
case intro.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w

case intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
all_goals
  simp_all [modelCanSemImplyForm, evaluatePoint, F, P, relateSeq, TP, testsOfProgram]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
⊢ τ ∈ testsOfProgram (?'τ)
Tactic:
simp [testsOfProgram]
State after:
no goals

State before:
case intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
Tactic:
simp_all [modelCanSemImplyForm, evaluatePoint, F, P, relateSeq, TP, testsOfProgram]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
simp at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
cases v_γ_w
State after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
h✝ : relate M α v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
h✝ : relate M β v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
case inl v_α_w =>
  have v_Fℓα : evaluate M v (Con (F α ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
  have IHα := existsBoxFP α v_α_w ℓ v_Fℓα rcases IHα with ⟨δ, _⟩
  use δ
  simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
case inr v_β_w =>
  have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
  have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ rcases IHβ with ⟨δ, _⟩
  use δ
  simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓα : evaluate M v (Con (F α ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
have IHα := existsBoxFP α v_α_w ℓ v_Fℓα
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
IHα : ∃ δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
IHα : ∃ δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
rcases IHα with ⟨δ, _⟩
State after:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
use δ
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ δ ∈ P (α⋓β) ℓ ∧ relateSeq M δ v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ δ ∈ P (α⋓β) ℓ ∧ relateSeq M δ v w
Tactic:
simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
⊢ evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
IHβ : ∃ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
IHβ : ∃ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
rcases IHβ with ⟨δ, _⟩
State after:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w

State before:
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
Tactic:
use δ
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ δ ∈ P (α⋓β) ℓ ∧ relateSeq M δ v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ δ ∈ P (α⋓β) ℓ ∧ relateSeq M δ v w
Tactic:
simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_β_w : relate M β v w
⊢ evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α;'β) v w
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
simp only [relate] at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
rcases v_γ_w with ⟨u, v_α_u, u_β_w⟩
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓα : evaluate M v (Con (F α ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
have IHα := existsBoxFP α v_α_u ℓ v_Fℓα
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
IHα : ∃ δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
IHα : ∃ δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
rcases IHα with ⟨δ, ⟨δ_in, v_δ_u⟩⟩
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
cases em (δ = [])
State after:
case intro.intro.intro.intro.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

case intro.intro.intro.intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
hyp : δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
case inl hyp =>
  subst hyp
  simp [relateSeq] at v_δ_u
  subst v_δ_u
  rename relate M β v w => v_β_w
  have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
  have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ rcases IHβ with ⟨η, ⟨η_in, v_η_w⟩⟩
  use η
  simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
hyp : δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
subst hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M [] v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M [] v u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
simp [relateSeq] at v_δ_u
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : v = u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : v = u
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
subst v_δ_u
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
u_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
u_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
rename relate M β v w => v_β_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
IHβ : ∃ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
IHβ : ∃ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩, relateSeq M δ v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
rcases IHβ with ⟨η, ⟨η_in, v_η_w⟩⟩
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
use η
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ η ∈ P (α;'β) ℓ ∧ relateSeq M η v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
v_Fℓβ : evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
η : List Program
η_in : η ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
v_η_w : relateSeq M η v w
⊢ η ∈ P (α;'β) ℓ ∧ relateSeq M η v w
Tactic:
simp_all [P]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
⊢ evaluate M v (Con (F β fun τ => ℓ ⟨↑τ, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
Tactic:
use δ ++ [β]
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ++ [β] ∈ P (α;'β) ℓ ∧ relateSeq M (δ ++ [β]) v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ++ [β] ∈ P (α;'β) ℓ ∧ relateSeq M (δ ++ [β]) v w
Tactic:
simp_all [P, relateSeq]
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
      δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []) ∧
    relateSeq M (δ ++ [β]) v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
      δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []) ∧
    relateSeq M (δ ++ [β]) v w
Tactic:
constructor
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
    δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ relateSeq M (δ ++ [β]) v w

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨
    δ ++ [β] ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
Tactic:
left
State after:
case h.left.h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)

State before:
case h.left.h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
Tactic:
apply List.mem_filter_of_mem δ_in (by aesop)
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ (δ != []) = true
Tactic:
aesop
State after:
no goals

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ relateSeq M (δ ++ [β]) v w
Tactic:
simp [relateSeq_append]
State after:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Tactic:
use u
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : relate M (∗β) v w
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
simp only [relate] at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
cases ReflTransGen.cases_tail_eq_neq v_γ_w
State after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_is_w : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
case inl v_is_w =>
  subst v_is_w
  use []
  simp_all [P,relateSeq]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_is_w : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
subst v_is_w
State after:
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v v

State before:
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v v
Tactic:
use []
State after:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ [] ∈ P (∗β) ℓ ∧ relateSeq M [] v v

State before:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ [] ∈ P (∗β) ℓ ∧ relateSeq M [] v v
Tactic:
simp_all [P,relateSeq]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
hyp : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
rcases hyp with ⟨v_neq_w, ⟨u, v_neq_u, v_β_u, u_βS_w⟩⟩
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have IHβ := existsBoxFP β v_β_u ℓ v_Fℓβ
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
IHβ :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
IHβ :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
rcases IHβ with ⟨δ, ⟨δ_in, v_δ_w⟩⟩
State after:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
have claim : δ ≠ [] := by by_contra hyp; subst hyp; simp_all [relateSeq];
State after:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w

State before:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
Tactic:
use δ ++ [∗β]
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ δ ++ [∗β] ∈ P (∗β) ℓ ∧ relateSeq M (δ ++ [∗β]) v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : δ ≠ []
⊢ δ ++ [∗β] ∈ P (∗β) ℓ ∧ relateSeq M (δ ++ [∗β]) v w
Tactic:
simp_all [P, relateSeq]
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩) ∧ relateSeq M (δ ++ [∗β]) v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩) ∧ relateSeq M (δ ++ [∗β]) v w
Tactic:
constructor
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ relateSeq M (δ ++ [∗β]) v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
Tactic:
simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
⊢ δ ≠ []
Tactic:
by_contra hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
hyp : δ = []
⊢ False

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M δ v u
hyp : δ = []
⊢ False
Tactic:
subst hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M [] v u
⊢ False

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ_in :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
v_δ_w : relateSeq M [] v u
⊢ False
Tactic:
simp_all [relateSeq]
State after:
no goals

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
Tactic:
apply List.mem_filter_of_mem δ_in (by aesop)
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ (δ != []) = true
Tactic:
aesop
State after:
no goals

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ relateSeq M (δ ++ [∗β]) v w
Tactic:
simp [relateSeq_append]
State after:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ Relation.ReflTransGen (relate M β) u w

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ Relation.ReflTransGen (relate M β) u w
Tactic:
use u
State after:
no goals