---

Step * 1 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 : runEvents(r)@i
5. y : runEvents(r)@i
6. x run-lt(r) y@i
⊢ run-event-step(x) < run-event-step(y)
BY
{ EAuto 1 }

---

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.  x  :  runEvents(r)@i
5.  y  :  runEvents(r)@i
6.  x  run-lt(r)  y@i
\mvdash{}  run-event-step(x)  <  run-event-step(y)


By

---

Latex:
EAuto  1

---

Home Index