---

Step * 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
⊢ ∃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))))
⇐⇒ (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
{ (D 0 THEN (D 0 THENA Auto) THEN ExRepD) }

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

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

---

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
\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)>)))
\mLeftarrow{}{}\mRightarrow{}  (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:
(D  0  THEN  (D  0  THENA  Auto)  THEN  ExRepD)

---

Home Index