Theorem: existsWitnessPath_ltr (Pdl/Paths.lean)

State before:
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
induction δ generalizing v
State after:
case nil
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)

case cons
W : Type
M : KripkeModel W
ξ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ (v : W), evaluate M v (~⌈⌈tail✝⌉⌉ξ) → Nonempty (witness M v tail✝ ξ)
v : W
⊢ evaluate M v (~⌈⌈head✝ :: tail✝⌉⌉ξ) → Nonempty (witness M v (head✝ :: tail✝) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)
Tactic:
case nil =>
  intro v_ξ
  constructor
  apply witness.nil
  simp at *
  exact v_ξ
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ) → Nonempty (witness M v (α :: γs) ξ)
Tactic:
case cons α γs IH =>
  intro v_
  simp at *
  rcases v_ with ⟨w, v_α_w, w_⟩
  rcases IH w w_ with ⟨w_wit⟩
  cases α case atom_prog a =>
    simp at v_α_w
    constructor
    apply witness.consAtom v_α_w w_wit
  case sequence α β =>
    simp at *
    rcases v_α_w with ⟨u, v_u, u_w⟩
    rcases IH w w_ with ⟨w_wit⟩
    constructor
    sorry
  case union α β =>
    constructor
    sorry
  case test τ =>
    constructor
    sorry
  case star β =>
    constructor
    sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ) → Nonempty (witness M v [] ξ)
Tactic:
intro v_ξ
State after:
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ Nonempty (witness M v [] ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ Nonempty (witness M v [] ξ)
Tactic:
constructor
State after:
case val
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ witness M v [] ξ

State before:
case val
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ witness M v [] ξ
Tactic:
apply witness.nil
State after:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ evaluate M v (~ξ)

State before:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : evaluate M v (~⌈⌈[]⌉⌉ξ)
⊢ evaluate M v (~ξ)
Tactic:
simp at *
State after:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ

State before:
case val.a
W : Type
M : KripkeModel W
ξ : Formula
v : W
v_ξ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ
Tactic:
exact v_ξ
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ) → Nonempty (witness M v (α :: γs) ξ)
Tactic:
intro v_
State after:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
v_ : evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
v_ : evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
simp at *
State after:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v_ : ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v_ : ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
rcases v_ with ⟨w, v_α_w, w_⟩
State after:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)

State before:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
rcases IH w w_ with ⟨w_wit⟩
State after:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v (α :: γs) ξ)

State before:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v (α :: γs) ξ)
Tactic:
cases α
State after:
case intro.intro.intro.atom_prog
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : ℕ
v_α_w : relate M (·a✝) v w
⊢ Nonempty (witness M v ((·a✝) :: γs) ξ)

case intro.intro.intro.sequence
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹;'a✝) v w
⊢ Nonempty (witness M v ((a✝¹;'a✝) :: γs) ξ)

case intro.intro.intro.union
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹⋓a✝) v w
⊢ Nonempty (witness M v ((a✝¹⋓a✝) :: γs) ξ)

case intro.intro.intro.star
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : Program
v_α_w : relate M (∗a✝) v w
⊢ Nonempty (witness M v ((∗a✝) :: γs) ξ)

case intro.intro.intro.test
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a✝ : Formula
v_α_w : relate M (?'a✝) v w
⊢ Nonempty (witness M v ((?'a✝) :: γs) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : relate M (·a) v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
case atom_prog a =>
  simp at v_α_w
  constructor
  apply witness.consAtom v_α_w w_wit
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α;'β) v w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
case sequence α β =>
  simp at *
  rcases v_α_w with ⟨u, v_u, u_w⟩
  rcases IH w w_ with ⟨w_wit⟩
  constructor
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ Nonempty (witness M v ((α⋓β) :: γs) ξ)
Tactic:
case union α β =>
  constructor
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ Nonempty (witness M v ((?'τ) :: γs) ξ)
Tactic:
case test τ =>
  constructor
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ Nonempty (witness M v ((∗β) :: γs) ξ)
Tactic:
case star β =>
  constructor
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : relate M (·a) v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
simp at v_α_w
State after:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ Nonempty (witness M v ((·a) :: γs) ξ)
Tactic:
constructor
State after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ witness M v ((·a) :: γs) ξ

State before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
a : ℕ
v_α_w : M.Rel a v w
⊢ witness M v ((·a) :: γs) ξ
Tactic:
apply witness.consAtom v_α_w w_wit
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α;'β) v w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
simp at *
State after:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
rcases v_α_w with ⟨u, v_u, u_w⟩
State after:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)

State before:
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
rcases IH w w_ with ⟨w_wit⟩
State after:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)

State before:
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v ((α;'β) :: γs) ξ)
Tactic:
constructor
State after:
case intro.intro.intro.val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ witness M v ((α;'β) :: γs) ξ

State before:
case intro.intro.intro.val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit✝ : witness M w γs ξ
α β : Program
u : W
v_u : relate M α v u
u_w : relate M β u w
w_wit : witness M w γs ξ
⊢ witness M v ((α;'β) :: γs) ξ
Tactic:
sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ Nonempty (witness M v ((α⋓β) :: γs) ξ)
Tactic:
constructor
State after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ witness M v ((α⋓β) :: γs) ξ

State before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
α β : Program
v_α_w : relate M (α⋓β) v w
⊢ witness M v ((α⋓β) :: γs) ξ
Tactic:
sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ Nonempty (witness M v ((?'τ) :: γs) ξ)
Tactic:
constructor
State after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ witness M v ((?'τ) :: γs) ξ

State before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
τ : Formula
v_α_w : relate M (?'τ) v w
⊢ witness M v ((?'τ) :: γs) ξ
Tactic:
sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ Nonempty (witness M v ((∗β) :: γs) ξ)
Tactic:
constructor
State after:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ witness M v ((∗β) :: γs) ξ

State before:
case val
W : Type
M : KripkeModel W
ξ : Formula
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
β : Program
v_α_w : relate M (∗β) v w
⊢ witness M v ((∗β) :: γs) ξ
Tactic:
sorry
State after:
no goals