Theorem: relateSeq_toChain' (Pdl/Unfold.lean)

State before:
W : Type
M : KripkeModel W
δ : List Program
v w : W
⊢ relateSeq M δ v w → δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
Tactic:
induction δ generalizing v w
State after:
case nil
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))

case cons
W : Type
M : KripkeModel W
head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ {v w : W},
    relateSeq M tail✝ v w →
      tail✝ ≠ [] → ∃ l, l.length + 1 = tail✝.length ∧ List.Chain' (pairRel M) (((?'⊤) :: tail✝).zip (v :: l ++ [w]))
v w : W
⊢ relateSeq M (head✝ :: tail✝) v w →
    head✝ :: tail✝ ≠ [] →
      ∃ l,
        l.length + 1 = (head✝ :: tail✝).length ∧ List.Chain' (pairRel M) (((?'⊤) :: head✝ :: tail✝).zip (v :: l ++ [w]))

State before:
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
Tactic:
case nil =>
  simp [relateSeq]
State after:
no goals

State before:
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
Tactic:
simp [relateSeq]
State after:
no goals

State before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
cases em (δ = [])
State after:
case inl
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
h✝ : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

case inr
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
h✝ : ¬δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

State before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_eq_empty : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
case inl δ_eq_empty =>
  subst δ_eq_empty
  intro _
  simp_all [pairRel]
State after:
no goals

State before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_eq_empty : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
subst δ_eq_empty
State after:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
⊢ relateSeq M [e] v w →
    [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))

State before:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
⊢ relateSeq M [e] v w →
    [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Tactic:
intro _
State after:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
a✝ : relateSeq M [e] v w
⊢ [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))

State before:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
a✝ : relateSeq M [e] v w
⊢ [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Tactic:
simp_all [pairRel]
State after:
no goals

State before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
simp only [relateSeq]
State after:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ (∃ u, relate M e v u ∧ relateSeq M δ u w) →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

State before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ (∃ u, relate M e v u ∧ relateSeq M δ u w) →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
rintro ⟨u, v_d_u, u_δ_w⟩ _
State after:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

State before:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
specialize IH u_δ_w δ_notEmpty
State after:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
IH : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

State before:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
IH : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
rcases IH with ⟨l, l_def, lchain⟩
State after:
case intro.intro.intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

State before:
case intro.intro.intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
use (u :: l)
State after:
case h
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))

State before:
case h
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Tactic:
constructor
State after:
case h.left
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length

case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))

State before:
case h.left
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length
Tactic:
simp_all
State after:
no goals

State before:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Tactic:
simp_all [pairRel]
State after:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) ((e, u) :: δ.zip (l ++ [w]))

State before:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) ((e, u) :: δ.zip (l ++ [w]))
Tactic:
apply List.Chain'.cons'
State after:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))

case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ ∀ y ∈ (δ.zip (l ++ [w])).head?, pairRel M (e, u) y

State before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))
Tactic:
have := List.Chain'.tail lchain
State after:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
this : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w])).tail
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))

State before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
this : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w])).tail
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))
Tactic:
simp_all
State after:
no goals

State before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ ∀ y ∈ (δ.zip (l ++ [w])).head?, pairRel M (e, u) y
Tactic:
cases l <;> cases δ
State after:
case h.right.a.nil.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : [].length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip ([] ++ [w]))
⊢ ∀ y ∈ ([].zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.nil.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : [].length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip ([] ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : W
tail✝ : List W
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : (head✝ :: tail✝).length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip (head✝ :: tail✝ ++ [w]))
⊢ ∀ y ∈ ([].zip (head✝ :: tail✝ ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y

State before:
case h.right.a.nil.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : [].length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip ([] ++ [w]))
⊢ ∀ y ∈ ([].zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.nil.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : [].length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip ([] ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : W
tail✝ : List W
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : (head✝ :: tail✝).length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip (head✝ :: tail✝ ++ [w]))
⊢ ∀ y ∈ ([].zip (head✝ :: tail✝ ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
Tactic:
all_goals simp_all [pairRel]
State after:
no goals

State before:
case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
Tactic:
simp_all [pairRel]
State after:
no goals