---

Step * of Lemma hdf-parallel-bag-iterate

∀[A,B:Type]. ∀[Xs:bag(hdataflow(A;B))]. ∀[inputs:A List].
  hdf-parallel-bag(Xs)*(inputs) = hdf-parallel-bag(bag-map(λx.x*(inputs);Xs)) ∈ hdataflow(A;B) 
  supposing valueall-type(B)
BY
{ (Auto
   THEN MoveToConcl (-3)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete ((RWO "bag-map-trivial" 0 THEN Auto)))
   THEN RW (AddrC [2] (UnfoldC `hdf-parallel-bag`)) 0
   THEN RecUnfold `mk-hdf` 0
   THEN Fold `hdf-parallel-bag` 0
   THEN Repeat (AutoSplit)
   THEN Reduce 0
   THEN Try ((RWO "iterate-hdf-halt" 0 THENA Complete (Auto)))
   THEN Try (Complete (Auto))) }

1
1. A : Type
2. B : Type
3. valueall-type(B)
4. u : A@i
5. v : A List@i
6. ∀Xs:bag(hdataflow(A;B)). (hdf-parallel-bag(Xs)*(v) = hdf-parallel-bag(bag-map(λx.x*(v);Xs)) ∈ hdataflow(A;B))@i
7. Xs : bag(hdataflow(A;B))@i
8. ↑bag_all(Xs;λx.hdf-halted(x))
⊢ hdf-halt() = hdf-parallel-bag(bag-map(λx.fst(x(u))*(v);Xs)) ∈ hdataflow(A;B)

2
1. A : Type
2. B : Type
3. valueall-type(B)
4. u : A@i
5. v : A List@i
6. ∀Xs:bag(hdataflow(A;B)). (hdf-parallel-bag(Xs)*(v) = hdf-parallel-bag(bag-map(λx.x*(v);Xs)) ∈ hdataflow(A;B))@i
7. Xs : bag(hdataflow(A;B))@i
8. ¬↑bag_all(Xs;λx.hdf-halted(x))
⊢ fst(hdf-run(λa.let s1,b = eval x = bag-map(λX.X(a);Xs) in
                            let out ←─ ∪p∈x.snd(p)
                            in <bag-map(λp.(fst(p));x), out> 
                 in <hdf-parallel-bag(s1), b>)(u))*(v)
= hdf-parallel-bag(bag-map(λx.fst(x(u))*(v);Xs))
∈ hdataflow(A;B)

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[Xs:bag(hdataflow(A;B))].  \mforall{}[inputs:A  List].
    hdf-parallel-bag(Xs)*(inputs)  =  hdf-parallel-bag(bag-map(\mlambda{}x.x*(inputs);Xs)) 
    supposing  valueall-type(B)


By

(Auto
  THEN  MoveToConcl  (-3)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "bag-map-trivial"  0  THEN  Auto)))
  THEN  RW  (AddrC  [2]  (UnfoldC  `hdf-parallel-bag`))  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Fold  `hdf-parallel-bag`  0
  THEN  Repeat  (AutoSplit)
  THEN  Reduce  0
  THEN  Try  ((RWO  "iterate-hdf-halt"  0  THENA  Complete  (Auto)))
  THEN  Try  (Complete  (Auto)))

---

Home Index