---

Step * of Lemma hdf-compose1-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[f:B ─→ C]. ∀[a:A].
  f o X(a) ~ <f o (fst(X(a))), bag-map(f;snd(X(a)))> supposing valueall-type(C)
BY
{ (Auto
   THEN RepUR ``hdf-compose1 hdf-ap`` 0⋅
   THEN RW (AddrC [1] (RecUnfoldC `mk-hdf`)) 0
   THEN (Reduce 0
         THEN Fold `hdf-ap` 0
         THEN Repeat (AutoSplit)
         THEN HDataflowHDAll
         THEN Try (Complete ((RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Auto)))
         THEN (CallByValueReduceAtAddr [1;1] 0 THENA Auto)
         THEN Reduce 0
         THEN Auto)⋅) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[f:B  {}\mrightarrow{}  C].  \mforall{}[a:A].
    f  o  X(a)  \msim{}  <f  o  (fst(X(a))),  bag-map(f;snd(X(a)))>  supposing  valueall-type(C)


By

(Auto
  THEN  RepUR  ``hdf-compose1  hdf-ap``  0\mcdot{}
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `mk-hdf`))  0
  THEN  (Reduce  0
              THEN  Fold  `hdf-ap`  0
              THEN  Repeat  (AutoSplit)
              THEN  HDataflowHDAll
              THEN  Try  (Complete  ((RecUnfold  `mk-hdf`  0  THEN  Reduce  0  THEN  Auto)))
              THEN  (CallByValueReduceAtAddr  [1;1]  0  THENA  Auto)
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index