---

Step * of Lemma member-run-event-interval

∀[M:Type ⟶ Type]
  ∀r:pRunType(P.M[P]). ∀e1,e2,e:runEvents(r).
    ((e ∈ run-event-interval(r;e1;e2))
    ⇐⇒ (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
{ ((UnivCD THENA Auto)
   THEN RepUR ``run-event-interval let`` 0
   THEN ((RWO "member-mapfilter" 0 THENM Reduce 0)
         THENA (All Reduce THEN Auto THEN RepeatFor 2 (DVar `t') THEN MemTypeCD THEN Auto THEN 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
⊢ ∃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))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P]).  \mforall{}e1,e2,e:runEvents(r).
        ((e  \mmember{}  run-event-interval(r;e1;e2))
        \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:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``run-event-interval  let``  0
  THEN  ((RWO  "member-mapfilter"  0  THENM  Reduce  0)
              THENA  (All  Reduce  THEN  Auto  THEN  RepeatFor  2  (DVar  `t')  THEN  MemTypeCD  THEN  Auto  THEN  Auto')
              ))

---

Home Index