---

{ [A,B:Type]. [g:B  LabeledDAG(Id  (Com(P.A) Process(P.A)))]. [L:A List].
  [F:dataflow(A;B)].
    (data-stream(dataflow-to-Process(
                 F;
                 g);L) ~ map(g;data-stream(F;L))) }

{ Proof }

---

Definitions occuring in Statement :  dataflow-to-Process: dataflow-to-Process,  Process: Process(P.M[P]),  Com: Com(P.M[P]),  ldag: LabeledDAG(T),  data-stream: data-stream(P;L),  dataflow: dataflow(A;B),  Id: Id,  map: map(f;as),  uall: [x:A]. B[x],  apply: f a,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  dataflow-to-Process: dataflow-to-Process,  map: map(f;as),  rec-process: RecProcess(s0;s,m.next[s; m]),  member: t  T,  ycomb: Y,  so_lambda: x.t[x],  top: Top,  all: x:A. B[x],  subtype: S  T,  pi2: snd(t),  pi1: fst(t),  implies: P  Q,  so_apply: x[s]
Lemmas :  dataflow_wf,  ldag_wf,  Id_wf,  Com_wf,  Process_wf,  top_wf,  dataflow-ap_wf,  data-stream-cons

---

\mforall{}[A,B:Type].  \mforall{}[g:B  {}\mrightarrow{}  LabeledDAG(Id  \mtimes{}  (Com(P.A)  Process(P.A)))].  \mforall{}[L:A  List].  \mforall{}[F:dataflow(A;B)].
    (data-stream(dataflow-to-Process(
                              F;
                              g);L)  \msim{}  map(g;data-stream(F;L)))


Date html generated: 2011_08_16-PM-06_50_15
Last ObjectModification: 2011_06_18-AM-11_04_40

Home Index