---

Step * of Lemma datastream-dataflow-to-Process

∀[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)))
BY
{ ((Unfold `dataflow-to-Process` 0
    THEN (Unfold `rec-process` 0⋅ THEN Fold `rec-dataflow` 0)
    THEN (InductionOnList
          THEN Reduce 0
          THEN (UnivCD THENA Auto)
          THEN Try (Trivial)
          THEN ((RWO "data-stream-cons" 0 THEN Reduce 0) THENA Auto))⋅)
   THEN (GenConclAtAddr [1;1;1;1;1] THEN D -2 THEN Reduce 0 THEN EqCD THEN Try (Trivial) THEN BackThruSomeHyp)⋅
   ) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `dataflow-to-Process`  0
    THEN  (Unfold  `rec-process`  0\mcdot{}  THEN  Fold  `rec-dataflow`  0)
    THEN  (InductionOnList
                THEN  Reduce  0
                THEN  (UnivCD  THENA  Auto)
                THEN  Try  (Trivial)
                THEN  ((RWO  "data-stream-cons"  0  THEN  Reduce  0)  THENA  Auto))\mcdot{})
  THEN  (GenConclAtAddr  [1;1;1;1;1]
              THEN  D  -2
              THEN  Reduce  0
              THEN  EqCD
              THEN  Try  (Trivial)
              THEN  BackThruSomeHyp)\mcdot{}
  )

---

Home Index