---

Step * of Lemma run-event-in-transit_wf

∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)].
  (run-event-in-transit(r;e) ∈ LabeledGraph(pInTransit(P.M[P])))
BY
{ (Auto
   THEN D -1
   THEN MoveToConcl (-1)
   THEN D -1
   THEN RepUR ``run-event-in-transit is-run-event`` 0
   THEN GenConclAtAddr[1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Repeat (Thin (-1))
   THEN D -1
   THEN Reduce 0
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[e:runEvents(r)].
    (run-event-in-transit(r;e)  \mmember{}  LabeledGraph(pInTransit(P.M[P])))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  D  -1
  THEN  RepUR  ``run-event-in-transit  is-run-event``  0
  THEN  GenConclAtAddr[1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Repeat  (Thin  (-1))
  THEN  D  -1
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))

---

Home Index