---

Step * 1 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. y : {x:ℤ| (run-event-step(e1) ≤ x) ∧ x < run-event-step(e2) + 1} @i
7. (y ∈ [run-event-step(e1), run-event-step(e2) + 1))@i
8. ↑is-run-event(r;y;run-event-loc(e1))@i
9. e = <y, run-event-loc(e1)> ∈ runEvents(r)@i
⊢ (run-event-loc(e) = run-event-loc(e1) ∈ Id)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ (run-event-step(e) ≤ run-event-step(e2))
BY
{ (HypSubst' (-1) 0
   THEN Unfolds ``run-event-loc run-event-step`` 0
   THEN Reduce 0
   THEN Folds ``run-event-loc run-event-step`` 0
   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.  y  :  \{x:\mBbbZ{}|  (run-event-step(e1)  \mleq{}  x)  \mwedge{}  x  <  run-event-step(e2)  +  1\}  @i
7.  (y  \mmember{}  [run-event-step(e1),  run-event-step(e2)  +  1))@i
8.  \muparrow{}is-run-event(r;y;run-event-loc(e1))@i
9.  e  =  <y,  run-event-loc(e1)>@i
\mvdash{}  (run-event-loc(e)  =  run-event-loc(e1))
\mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e))
\mwedge{}  (run-event-step(e)  \mleq{}  run-event-step(e2))


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  Unfolds  ``run-event-loc  run-event-step``  0
  THEN  Reduce  0
  THEN  Folds  ``run-event-loc  run-event-step``  0
  THEN  Auto)

---

Home Index