---

{ [A,B:Type]. [df:dataflow(A;B)]. [a:A].  (df(a)  dataflow(A;B)  B) }

{ Proof }

---

Definitions occuring in Statement :  dataflow-ap: df(a),  dataflow: dataflow(A;B),  uall: [x:A]. B[x],  member: t  T,  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  dataflow-ap: df(a),  all: x:A. B[x],  implies: P  Q,  ext-eq: A  B,  and: P  Q
Lemmas :  dataflow_wf,  dataflow-ext-eq

---

\mforall{}[A,B:Type].  \mforall{}[df:dataflow(A;B)].  \mforall{}[a:A].    (df(a)  \mmember{}  dataflow(A;B)  \mtimes{}  B)


Date html generated: 2011_08_10-AM-08_14_10
Last ObjectModification: 2011_06_18-AM-08_29_44

Home Index