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