---

Step * of Lemma dataflow-to-Process_functionality

∀[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
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepUR ``Process-stream`` 0
   THEN RWO "datastream-dataflow-to-Process" 0
   THEN Try (Complete (Auto))) }

1
1. A : Type
2. B : Type
3. F1 : dataflow(A;B)
4. F2 : dataflow(A;B)
5. g : B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))
6. F1 ≡ F2
7. msgs : pMsg(P.A) List@i
⊢ map(g;data-stream(F1;msgs)) = map(g;data-stream(F2;msgs)) ∈ (pExt(P.A) List)

---

Latex:

---

Latex:
\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


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``Process-stream``  0
  THEN  RWO  "datastream-dataflow-to-Process"  0
  THEN  Try  (Complete  (Auto)))

---

Home Index