---

{ [M:Type  Type]. [r:pRunType(P.M[P])]. [e:runEvents(r)].
    (run-event-msg(r;e)  pMsg(P.M[P])) }

{ Proof }

---

Definitions occuring in Statement :  run-event-msg: run-event-msg(r;e),  runEvents: runEvents(r),  pRunType: pRunType(T.M[T]),  pMsg: pMsg(P.M[P]),  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],  so_apply: x[s],  member: t  T,  run-event-msg: run-event-msg(r;e),  so_lambda: x.t[x]
Lemmas :  pi2_wf,  Id_wf,  pMsg_wf,  run-info_wf,  runEvents_wf,  pRunType_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[e:runEvents(r)].    (run-event-msg(r;e)  \mmember{}  pMsg(P.M[P]))


Date html generated: 2011_08_16-PM-06_57_35
Last ObjectModification: 2011_06_18-AM-11_12_42

Home Index