---

{ [msgs:Message List]. [P:Proc].  (Process-stream(P;msgs)  ProcOut List) }

{ Proof }

---

Definitions occuring in Statement :  ProcOut: ProcOut,  Proc: Proc,  Message: Message,  Process-stream: Process-stream(P;msgs),  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  Message: Message,  member: t  T,  ProcOut: ProcOut,  pMsg: pMsg(P.M[P]),  so_lambda: x.t[x],  Proc: Proc,  uimplies: b supposing a,  so_apply: x[s]
Lemmas :  Process-stream_wf,  name_wf,  mData_wf,  Proc_wf,  Message_wf,  strong-continuous-product,  continuous-constant

---

\mforall{}[msgs:Message  List].  \mforall{}[P:Proc].    (Process-stream(P;msgs)  \mmember{}  ProcOut  List)


Date html generated: 2011_08_17-PM-04_12_23
Last ObjectModification: 2011_06_18-AM-11_30_29

Home Index