---

Step * 1 1 of Lemma hdf-parallel-bind-halt-eq


1. A : Type
2. B : Type
3. C : Type
4. valueall-type(B)
5. valueall-type(C)
6. X1 : hdataflow(A;B)@i
7. X2 : hdataflow(A;B)@i
8. X : B ─→ hdataflow(A;C)@i
9. hdfs1 : bag(hdataflow(A;C))@i
10. hdfs2 : bag(hdataflow(A;C))@i
⊢ hdf-halted(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X) = hdf-halted(X1 || X2 (hdfs1 + hdfs2) >>= X)
BY
{ (RepUR ``hdf-bind-gen hdf-parallel bind-nxt`` 0⋅
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN (All(\h.RWO "bag-append-eq-empty" h THENA Complete Auto)⋅
         THEN Auto
         THEN OnMaybeHyp 12 (\h. (D h THEN Complete (Auto))))⋅) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  valueall-type(B)
5.  valueall-type(C)
6.  X1  :  hdataflow(A;B)@i
7.  X2  :  hdataflow(A;B)@i
8.  X  :  B  {}\mrightarrow{}  hdataflow(A;C)@i
9.  hdfs1  :  bag(hdataflow(A;C))@i
10.  hdfs2  :  bag(hdataflow(A;C))@i
\mvdash{}  hdf-halted(X1  (hdfs1)  >>=  X  ||  X2  (hdfs2)  >>=  X)  =  hdf-halted(X1  ||  X2  (hdfs1  +  hdfs2)  >>=  X)


By

---

Latex:
(RepUR  ``hdf-bind-gen  hdf-parallel  bind-nxt``  0\mcdot{}
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  (All(\mbackslash{}h.RWO  "bag-append-eq-empty"  h  THENA  Complete  Auto)\mcdot{}
              THEN  Auto
              THEN  OnMaybeHyp  12  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))\mcdot{})

---

Home Index