---

Step * of Lemma run_local_pred_time_less

∀M:Type ─→ Type. ∀r:pRunType(P.M[P]). ∀e,x:runEvents(r).
  ((run-event-loc(x) = run-event-loc(e) ∈ Id)
  ⇒ run-event-step(x) < run-event-step(e)
  ⇒ run-event-step(run_local_pred(r;e)) < run-event-step(e))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN RepeatFor 2 ((D -1 THEN (D -2 THEN RepUR ``run-event-loc run-event-step`` 0) THEN (D 0 THENA Auto)))
   THEN All Reduce
   THEN Auto
   THEN RepUR ``run_local_pred`` 0) }

1
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x2 = e2 ∈ Id@i
10. x1 < e1@i
⊢ fst(run-local-pred(r;e2;e1;e1)) < e1

---

Latex:

---

Latex:
\mforall{}M:Type  {}\mrightarrow{}  Type.  \mforall{}r:pRunType(P.M[P]).  \mforall{}e,x:runEvents(r).
    ((run-event-loc(x)  =  run-event-loc(e))
    {}\mRightarrow{}  run-event-step(x)  <  run-event-step(e)
    {}\mRightarrow{}  run-event-step(run\_local\_pred(r;e))  <  run-event-step(e))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  ((D  -1
                                        THEN  (D  -2  THEN  RepUR  ``run-event-loc  run-event-step``  0)
                                        THEN  (D  0  THENA  Auto)))
  THEN  All  Reduce
  THEN  Auto
  THEN  RepUR  ``run\_local\_pred``  0)

---

Home Index