---

{ [M:Type  Type]. [r:pRunType(P.M[P])]. [t:].
    (run-intransit(r;t)  LabeledDAG(pInTransit(P.M[P]))) }

{ Proof }

---

Definitions occuring in Statement :  run-intransit: run-intransit(r;t),  pRunType: pRunType(T.M[T]),  pInTransit: pInTransit(P.M[P]),  ldag: LabeledDAG(T),  nat_plus: ,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  pRunType: pRunType(T.M[T]),  so_apply: x[s],  member: t  T,  run-intransit: run-intransit(r;t),  nat: ,  run-system: run-system(r;t),  so_lambda: x.t[x],  le: A  B,  not: A,  implies: P  Q,  false: False,  nat_plus: ,  prop:
Lemmas :  pi2_wf,  top_wf,  ldag_wf,  pInTransit_wf,  Id_wf,  pMsg_wf,  unit_wf,  le_wf,  nat_plus_wf,  nat_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].
    (run-intransit(r;t)  \mmember{}  LabeledDAG(pInTransit(P.M[P])))


Date html generated: 2011_08_16-PM-06_56_47
Last ObjectModification: 2011_06_18-AM-11_10_45

Home Index