---

{ [T:ValueAllType]. [hdr:Name].
    (base-prog(T;hdr)  DataflowProgram(Message)) }

{ Proof }

---

Definitions occuring in Statement :  base-prog: base-prog(T;hdr),  Message: Message,  dataflow-program: DataflowProgram(A),  name: Name,  uall: [x:A]. B[x],  member: t  T,  vatype: ValueAllType
Lemmas :  equal-valueall-type,  subtype_rel_wf,  name_wf,  vatype_wf,  it_wf,  cond-msg-body_wf,  Message_wf,  bag_wf,  unit_wf,  member_wf,  valueall-type_wf

---

\mforall{}[T:ValueAllType].  \mforall{}[hdr:Name].    (base-prog(T;hdr)  \mmember{}  DataflowProgram(Message))


Date html generated: 2011_08_17-PM-04_01_24
Last ObjectModification: 2011_06_29-PM-11_47_17

Home Index