---

Step * 1 of Lemma dataflow-to-Process_functionality


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)
BY
{ (RepUR  ``pMsg`` (-1)⋅ THEN (With  ⌈msgs⌉ (D (-2))⋅ THENA Auto) THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  F1  :  dataflow(A;B)
4.  F2  :  dataflow(A;B)
5.  g  :  B  {}\mrightarrow{}  LabeledDAG(Id  \mtimes{}  (Com(P.A)  Process(P.A)))
6.  F1  \mequiv{}  F2
7.  msgs  :  pMsg(P.A)  List@i
\mvdash{}  map(g;data-stream(F1;msgs))  =  map(g;data-stream(F2;msgs))


By

---

Latex:
(RepUR    ``pMsg``  (-1)\mcdot{}  THEN  (With    \mkleeneopen{}msgs\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index