---

Step * 1 2 1 of Lemma member-run-event-interval


1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. e : runEvents(r)@i
6. run-event-loc(e) = run-event-loc(e1) ∈ Id@i
7. run-event-step(e1) ≤ run-event-step(e)@i
8. run-event-step(e) ≤ run-event-step(e2)@i
⊢ (run-event-step(e) ∈ [run-event-step(e1), run-event-step(e2) + 1))
∧ ((↑is-run-event(r;run-event-step(e);run-event-loc(e1)))
  c∧ (e = <run-event-step(e), run-event-loc(e1)> ∈ runEvents(r)))
BY
{ (RevHypSubst' (-3) 0
   THEN Auto
   THEN Try ((BLemma `member-from-upto` THEN Auto))
   THEN All Thin
   THEN RepUR ``run-event-step run-event-loc`` 0
   THEN RepeatFor 2 (DVar `e')
   THEN All Reduce
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  e1  :  runEvents(r)@i
4.  e2  :  runEvents(r)@i
5.  e  :  runEvents(r)@i
6.  run-event-loc(e)  =  run-event-loc(e1)@i
7.  run-event-step(e1)  \mleq{}  run-event-step(e)@i
8.  run-event-step(e)  \mleq{}  run-event-step(e2)@i
\mvdash{}  (run-event-step(e)  \mmember{}  [run-event-step(e1),  run-event-step(e2)  +  1))
\mwedge{}  ((\muparrow{}is-run-event(r;run-event-step(e);run-event-loc(e1)))
    c\mwedge{}  (e  =  <run-event-step(e),  run-event-loc(e1)>))


By

---

Latex:
(RevHypSubst'  (-3)  0
  THEN  Auto
  THEN  Try  ((BLemma  `member-from-upto`  THEN  Auto))
  THEN  All  Thin
  THEN  RepUR  ``run-event-step  run-event-loc``  0
  THEN  RepeatFor  2  (DVar  `e')
  THEN  All  Reduce
  THEN  Unhide
  THEN  Auto)

---

Home Index