---

Step * of Lemma hdf-parallel-ap

∀[A,B:Type]. ∀[X,Y:hdataflow(A;B)]. ∀[a:A].
  X || Y(a) = <fst(X(a)) || fst(Y(a)), (snd(X(a))) + (snd(Y(a)))> ∈ (hdataflow(A;B) × bag(B)) supposing valueall-type(B)
BY
{ (Auto
   THEN RepUR ``hdf-parallel hdf-ap`` 0
   THEN RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
   THEN Reduce 0
   THEN Fold `hdf-ap` 0
   THEN Repeat (AutoSplit)
   THEN HDataflowHDAll
   THEN Try ((CallByValueReduceAtAddr [2;1] 0 THENA Auto))
   THEN Reduce 0
   THEN Try (Complete ((RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Auto)))
   THEN Try (Complete ((Fold `hdf-parallel` 0 THEN Auto)))) }

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[X,Y:hdataflow(A;B)].  \mforall{}[a:A].
    X  ||  Y(a)  =  <fst(X(a))  ||  fst(Y(a)),  (snd(X(a)))  +  (snd(Y(a)))>  supposing  valueall-type(B)


By

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

---

Home Index