internlm/Lean-Github huggingface dataset:
Theorem: localBoxTruth
Proof state before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
this : evaluate M w ((⌈γ⌉ψ)⋀signature γ ℓ) ↔ evaluate M w (Con (Xset γ ℓ ψ)⋀signature γ ℓ)
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
sorry
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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 γ
Proof 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
Theorem: existsBoxFP
Proof 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
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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 *
Proof 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
Theorem: existsBoxFP
Proof 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
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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_τ⟩
Proof 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
Theorem: existsBoxFP
Proof 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]⟩ )
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof 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
Theorem: existsBoxFP
Proof 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ℓα
Proof 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
Theorem: existsBoxFP
Proof 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 ⟨δ, _⟩
Proof 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
Theorem: existsBoxFP
Proof 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 δ
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof 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
Theorem: existsBoxFP
Proof 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ℓβ
Proof 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
Theorem: existsBoxFP
Proof 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 ⟨δ, _⟩
Proof 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
Theorem: existsBoxFP
Proof 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 δ
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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⟩
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof 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
Theorem: existsBoxFP
Proof 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ℓα
Proof 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
Theorem: existsBoxFP
Proof 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⟩⟩
Proof 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
Theorem: existsBoxFP
Proof 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 (δ = [])
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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]
Proof state after:
no goals
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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
Proof 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
Theorem: existsBoxFP
Proof 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]
Proof 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
Theorem: existsBoxFP
Proof 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ℓβ
Proof 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