---

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


1. A : Type
2. B : Type
3. C : Type
4. X1 : hdataflow(A;B)
5. X2 : hdataflow(A;B)
6. X : B ─→ hdataflow(A;C)
7. valueall-type(B)
8. valueall-type(C)
9. inputs : A List@i
⊢ hdf-halted(X1 >>= X || X2 >>= X*(inputs)) = hdf-halted(X1 || X2 >>= X*(inputs))
BY
{ (RepUR ``hdf-bind`` 0
   THEN (GenConcl ⌈{} = hdfs1 ∈ bag(hdataflow(A;C))⌉ THENA Auto)
   THEN Fold `hdf-bind-gen` 0
   THEN (Assert ⌈∃hdfs2:bag(hdataflow(A;C)). (hdfs2 = {} ∈ bag(hdataflow(A;C)))⌉⋅ THENA (InstConcl [⌈{}⌉]⋅ THEN Auto))
   THEN D (-1)
   THEN (Subst ⌈X2 (hdfs1) >>= X = X2 (hdfs2) >>= X ∈ hdataflow(A;C)⌉ 0⋅ THENA Auto)
   THEN (Subst ⌈X1 || X2 (hdfs1) >>= X = X1 || X2 (hdfs1 + hdfs2) >>= X ∈ hdataflow(A;C)⌉ 0⋅
         THENA (Auto THEN SimpleSubstVar `hdfs1' 0 THEN (SimpleSubstVar `hdfs2' 0 THEN Reduce 0 THEN Auto))
         )
   THEN Thin (-1)
   THEN Thin (-2)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN RepeatFor 3 (MoveToConcl (-4))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (UnivCD THENA Auto))⋅ }

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

2
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. hdfs2 : bag(hdataflow(A;C))@i
⊢ hdf-halted(fst(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X(u))*(v)) = hdf-halted(fst(X1 || X2 (hdfs1 + hdfs2) >>= X(u))*(v))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``hdf-bind``  0
  THEN  (GenConcl  \mkleeneopen{}\{\}  =  hdfs1\mkleeneclose{}  THENA  Auto)
  THEN  Fold  `hdf-bind-gen`  0
  THEN  (Assert  \mkleeneopen{}\mexists{}hdfs2:bag(hdataflow(A;C)).  (hdfs2  =  \{\})\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}\{\}\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  D  (-1)
  THEN  (Subst  \mkleeneopen{}X2  (hdfs1)  >>=  X  =  X2  (hdfs2)  >>=  X\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}X1  ||  X2  (hdfs1)  >>=  X  =  X1  ||  X2  (hdfs1  +  hdfs2)  >>=  X\mkleeneclose{}  0\mcdot{}
              THENA  (Auto
                            THEN  SimpleSubstVar  `hdfs1'  0
                            THEN  (SimpleSubstVar  `hdfs2'  0  THEN  Reduce  0  THEN  Auto))
              )
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  RepeatFor  3  (MoveToConcl  (-4))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto))\mcdot{}

---

Home Index