---

Step * 1 2 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 (hdfs1) >>= X)
14. hdfs2 : bag(hdataflow(A;C))@i
15. ↑hdf-halted(X2 (hdfs2) >>= X)
⊢ hdf-halted(hdf-halt()*(v)) = hdf-halted(fst(X1 || X2 (hdfs1 + hdfs2) >>= X(u))*(v))
BY
{ ((RWO "iterate-hdf-halt" 0⋅ THENA Auto)
   THEN Reduce 0
   THEN AllHyps h.((RWO "hdf-bind-gen-halted" h
                    THENM RW assert_pushdownC h
                    THENM D h
                    THENM HypSubst' (h+1) 0
                    THENM FLemma `hdf-halted-is-halt` [h]
                    THENM HypSubst' (-1) 0)
                   THENA Auto
                   ) 
   THEN RWO "hdf-parallel-halt" 0
   THEN Reduce 0) }

1
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))

---

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  (hdfs1)  >>=  X)
14.  hdfs2  :  bag(hdataflow(A;C))@i
15.  \muparrow{}hdf-halted(X2  (hdfs2)  >>=  X)
\mvdash{}  hdf-halted(hdf-halt()*(v))  =  hdf-halted(fst(X1  ||  X2  (hdfs1  +  hdfs2)  >>=  X(u))*(v))


By

---

Latex:
((RWO  "iterate-hdf-halt"  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  AllHyps  h.((RWO  "hdf-bind-gen-halted"  h
                                    THENM  RW  assert\_pushdownC  h
                                    THENM  D  h
                                    THENM  HypSubst'  (h+1)  0
                                    THENM  FLemma  `hdf-halted-is-halt`  [h]
                                    THENM  HypSubst'  (-1)  0)
                                  THENA  Auto
                                  ) 
  THEN  RWO  "hdf-parallel-halt"  0
  THEN  Reduce  0)

---

Home Index