---

Step * of Lemma run-lt-transitive

∀[M:Type ⟶ Type]. ∀r:pRunType(P.M[P]). Trans(runEvents(r);x,y.x run-lt(r) y)
BY
{ (Auto THEN Unfold `run-lt` 0) }

1
1. [M] : Type ⟶ Type
2. r : pRunType(P.M[P])@i
⊢ Trans(runEvents(r);x,y.x run-pred(r)+ y)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}r:pRunType(P.M[P]).  Trans(runEvents(r);x,y.x  run-lt(r)  y)


By

---

Latex:
(Auto  THEN  Unfold  `run-lt`  0)

---

Home Index