---

Step * 1 2 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. u : A@i
7. v : A List@i
8. ∀X1,X2:hdataflow(A;B). ∀X:B ─→ hdataflow(A;C). ∀hdfs1,hdfs2:bag(hdataflow(A;C)).
     hdf-halted(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X*(v)) = hdf-halted(X1 || X2 (hdfs1 + hdfs2) >>= X*(v))@i
9. X1 : hdataflow(A;B)@i
10. X2 : hdataflow(A;B)@i
11. X : B ─→ hdataflow(A;C)@i
12. hdfs1 : bag(hdataflow(A;C))@i
13. ↑hdf-halted(X1)
14. hdfs1 = {} ∈ bag(hdataflow(A;C))
15. hdfs2 : bag(hdataflow(A;C))@i
16. ↑hdf-halted(X2)
17. hdfs2 = {} ∈ bag(hdataflow(A;C))
18. X2 ~ hdf-halt()
19. X1 ~ hdf-halt()
⊢ tt = hdf-halted(fst(hdf-halt() ({}) >>= X(u))*(v))
BY
{ ((RWO "hdf-bind-gen-halt-left" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "iterate-hdf-halt" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  valueall-type(B)
5.  valueall-type(C)
6.  u  :  A@i
7.  v  :  A  List@i
8.  \mforall{}X1,X2:hdataflow(A;B).  \mforall{}X:B  {}\mrightarrow{}  hdataflow(A;C).  \mforall{}hdfs1,hdfs2:bag(hdataflow(A;C)).
          hdf-halted(X1  (hdfs1)  >>=  X  ||  X2  (hdfs2)  >>=  X*(v))  =  hdf-halted(X1  ||  X2  (hdfs1  +  hdfs2)  >>=  \000CX*(v))@i
9.  X1  :  hdataflow(A;B)@i
10.  X2  :  hdataflow(A;B)@i
11.  X  :  B  {}\mrightarrow{}  hdataflow(A;C)@i
12.  hdfs1  :  bag(hdataflow(A;C))@i
13.  \muparrow{}hdf-halted(X1)
14.  hdfs1  =  \{\}
15.  hdfs2  :  bag(hdataflow(A;C))@i
16.  \muparrow{}hdf-halted(X2)
17.  hdfs2  =  \{\}
18.  X2  \msim{}  hdf-halt()
19.  X1  \msim{}  hdf-halt()
\mvdash{}  tt  =  hdf-halted(fst(hdf-halt()  (\{\})  >>=  X(u))*(v))


By

---

Latex:
((RWO  "hdf-bind-gen-halt-left"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "iterate-hdf-halt"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index