---

Step * 1 2 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
⊢ ∃y:{x:ℤ| (run-event-step(e1) ≤ x) ∧ x < run-event-step(e2) + 1} 
   ((y ∈ [run-event-step(e1), run-event-step(e2) + 1))
   ∧ ((↑is-run-event(r;y;run-event-loc(e1))) c∧ (e = <y, run-event-loc(e1)> ∈ runEvents(r))))
BY
{ (With ⌈run-event-step(e)⌉ (D 0)⋅ THENA Auto) }

1
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)))

---

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{}  \mexists{}y:\{x:\mBbbZ{}|  (run-event-step(e1)  \mleq{}  x)  \mwedge{}  x  <  run-event-step(e2)  +  1\} 
      ((y  \mmember{}  [run-event-step(e1),  run-event-step(e2)  +  1))
      \mwedge{}  ((\muparrow{}is-run-event(r;y;run-event-loc(e1)))  c\mwedge{}  (e  =  <y,  run-event-loc(e1)>)))


By

---

Latex:
(With  \mkleeneopen{}run-event-step(e)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)

---

Home Index