---

Step * 2 of Lemma hdf-parallel-bag-iterate


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)
BY
{ ((RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Try ((Reduce 0
              THEN (RWO "bag-map-map" 0 THENA Auto)
              THEN RepUR ``compose`` 0
              THEN (RWO "-3" 0 THENA Auto)
              THEN (RWO "bag-map-map" 0 THENA Auto)
              THEN RepUR ``compose`` 0
              THEN Auto))) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  valueall-type(B)
4.  u  :  A@i
5.  v  :  A  List@i
6.  \mforall{}Xs:bag(hdataflow(A;B)).  (hdf-parallel-bag(Xs)*(v)  =  hdf-parallel-bag(bag-map(\mlambda{}x.x*(v);Xs)))@i
7.  Xs  :  bag(hdataflow(A;B))@i
8.  \mneg{}\muparrow{}bag\_all(Xs;\mlambda{}x.hdf-halted(x))
\mvdash{}  fst(hdf-run(\mlambda{}a.let  s1,b  =  eval  x  =  bag-map(\mlambda{}X.X(a);Xs)  in
                                                        let  out  \mleftarrow{}{}  \mcup{}p\mmember{}x.snd(p)
                                                        in  <bag-map(\mlambda{}p.(fst(p));x),  out> 
                                  in  <hdf-parallel-bag(s1),  b>)(u))*(v)
=  hdf-parallel-bag(bag-map(\mlambda{}x.fst(x(u))*(v);Xs))


By

---

Latex:
((RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Try  ((Reduce  0
                        THEN  (RWO  "bag-map-map"  0  THENA  Auto)
                        THEN  RepUR  ``compose``  0
                        THEN  (RWO  "-3"  0  THENA  Auto)
                        THEN  (RWO  "bag-map-map"  0  THENA  Auto)
                        THEN  RepUR  ``compose``  0
                        THEN  Auto)))

---

Home Index