---

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

{ Proof }

---

Definitions occuring in Statement :  run-event-in-transit: run-event-in-transit(r;e),  runEvents: runEvents(r),  pRunType: pRunType(T.M[T]),  pInTransit: pInTransit(P.M[P]),  labeled-graph: LabeledGraph(T),  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-event-in-transit: run-event-in-transit(r;e),  is-run-event: is-run-event(r;t;x),  pi1: fst(t),  pi2: snd(t),  implies: P  Q,  spreadn: spread3,  so_lambda: x.t[x],  all: x:A. B[x],  assert: b,  band: p  q,  isl: isl(x),  outl: outl(x),  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  runEvents: runEvents(r),  ldag: LabeledDAG(T),  false: False,  prop:
Lemmas :  Id_wf,  pMsg_wf,  unit_wf,  top_wf,  ldag_wf,  pInTransit_wf,  runEvents_wf,  pRunType_wf,  assert_wf,  eq_id_wf,  false_wf

---

\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])))


Date html generated: 2011_08_16-PM-06_58_09
Last ObjectModification: 2011_06_18-AM-11_13_14

Home Index