---

Step * 1 of Lemma run-lt-transitive


1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
⊢ Trans(runEvents(r);x,y.x run-pred(r)+ y)
BY
{ (BLemma `rel_plus_trans` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
\mvdash{}  Trans(runEvents(r);x,y.x  run-pred(r)\msupplus{}  y)


By

---

Latex:
(BLemma  `rel\_plus\_trans`  THEN  Auto)\mcdot{}

---

Home Index