---

{ [A,B:Type]. [F1,F2:dataflow(A;B)].
  [g:B  LabeledDAG(Id  (Com(P.A) Process(P.A)))].
    dataflow-to-Process(F1;g)dataflow-to-Process(F2;g) supposing F1  F2 }

{ Proof }

---

Definitions occuring in Statement :  dataflow-to-Process: dataflow-to-Process,  process-equiv: process-equiv,  Process: Process(P.M[P]),  Com: Com(P.M[P]),  ldag: LabeledDAG(T),  dataflow-equiv: d1  d2,  dataflow: dataflow(A;B),  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  apply: f a,  function: x:A  B[x],  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  process-equiv: process-equiv,  member: t  T,  all: x:A. B[x],  pMsg: pMsg(P.M[P]),  Process-stream: Process-stream(P;msgs),  so_lambda: x.t[x],  subtype: S  T,  squash: T,  true: True,  suptype: suptype(S; T),  pExt: pExt(P.M[P]),  pCom: pCom(P.M[P]),  so_apply: x[s],  dataflow-equiv: d1  d2,  prop:
Lemmas :  pMsg_wf,  dataflow-equiv_wf,  ldag_wf,  Id_wf,  Com_wf,  Process_wf,  dataflow_wf,  datastream-dataflow-to-Process,  map_wf,  squash_wf,  true_wf,  pExt_wf

---

\mforall{}[A,B:Type].  \mforall{}[F1,F2:dataflow(A;B)].  \mforall{}[g:B  {}\mrightarrow{}  LabeledDAG(Id  \mtimes{}  (Com(P.A)  Process(P.A)))].
    dataflow-to-Process(F1;g)\mequiv{}dataflow-to-Process(F2;g)  supposing  F1  \mequiv{}  F2


Date html generated: 2011_08_16-PM-06_50_23
Last ObjectModification: 2011_06_18-AM-11_04_49

Home Index