---

Step * 1 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))
⊢ hdf-halt() = hdf-parallel-bag(bag-map(λx.fst(x(u))*(v);Xs)) ∈ hdataflow(A;B)
BY
{ (RepUR ``hdf-parallel-bag`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Subst' bag_all(bag-map(λx.fst(x(u))*(v);Xs);λx.hdf-halted(x)) ~ tt 0
   THEN Reduce 0
   THEN Auto
   THEN ((RWO "bag_all-map" 0 THENA Auto)
         THEN RepUR ``compose`` 0
         THEN (BLemma `eqtt_to_assert` THENA Auto)
         THEN BLemma `assert-bag_all`
         THEN Auto
         THEN (RepUR ``so_apply`` 0
               THEN (InstLemma `assert-bag_all` [⌈hdataflow(A;B)⌉;⌈λ2x.hdf-halted(x)⌉;⌈Xs⌉]⋅ THENA Auto)
               THEN RWO "-1<" (-4)
               THEN (InstHyp [⌈x⌉] (-4)⋅ THENA Auto)
               THEN (FLemma `hdf-halted-is-halt` [-1] THENA Auto)
               THEN RWO "-1" 0
               THEN Reduce 0
               THEN RWO "iterate-hdf-halt" 0
               THEN Reduce 0
               THEN Auto)⋅)⋅) }

---

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.  \muparrow{}bag\_all(Xs;\mlambda{}x.hdf-halted(x))
\mvdash{}  hdf-halt()  =  hdf-parallel-bag(bag-map(\mlambda{}x.fst(x(u))*(v);Xs))


By

(RepUR  ``hdf-parallel-bag``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Subst'  bag\_all(bag-map(\mlambda{}x.fst(x(u))*(v);Xs);\mlambda{}x.hdf-halted(x))  \msim{}  tt  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ((RWO  "bag\_all-map"  0  THENA  Auto)
              THEN  RepUR  ``compose``  0
              THEN  (BLemma  `eqtt\_to\_assert`  THENA  Auto)
              THEN  BLemma  `assert-bag\_all`
              THEN  Auto
              THEN  (RepUR  ``so\_apply``  0
                          THEN  (InstLemma  `assert-bag\_all`  [\mkleeneopen{}hdataflow(A;B)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.hdf-halted(x)\mkleeneclose{};\mkleeneopen{}Xs\mkleeneclose{}]\mcdot{}
                                      THENA  Auto
                                      )
                          THEN  RWO  "-1<"  (-4)
                          THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
                          THEN  (FLemma  `hdf-halted-is-halt`  [-1]  THENA  Auto)
                          THEN  RWO  "-1"  0
                          THEN  Reduce  0
                          THEN  RWO  "iterate-hdf-halt"  0
                          THEN  Reduce  0
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index