---

Step * 2 of Lemma run-eo_wf


1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
4. ∀x,y:runEvents(r).  ((↓x run-lt(r) y) ⇒ run-event-step(x) < run-event-step(y))
5. e : runEvents(r)@i
⊢ run-event-loc(run_local_pred(r;e)) = run-event-loc(e) ∈ Id
BY
{ (Unfold `run-event-loc` 0 THEN BLemma `run_local_pred_loc` THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)
4.  \mforall{}x,y:runEvents(r).    ((\mdownarrow{}x  run-lt(r)  y)  {}\mRightarrow{}  run-event-step(x)  <  run-event-step(y))
5.  e  :  runEvents(r)@i
\mvdash{}  run-event-loc(run\_local\_pred(r;e))  =  run-event-loc(e)


By

---

Latex:
(Unfold  `run-event-loc`  0  THEN  BLemma  `run\_local\_pred\_loc`  THEN  Auto)

---

Home Index