---

Step * 1 2 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. hdfs2 : bag(hdataflow(A;C))@i
14. ¬((↑hdf-halted(X1 (hdfs1) >>= X)) ∧ (↑hdf-halted(X2 (hdfs2) >>= X)))
⊢ hdf-halted(fst(let s1,b = let X',xs = X1 (hdfs1) >>= X(u) 
                            in let Y',ys = X2 (hdfs2) >>= X(u) 
                               in let out ←─ xs + ys
                                  in <<X', Y'>, out> 
                 in <mk-hdf(XY,a.let X,Y = XY 
                                 in let X',xs = X(a) 
                                    in let Y',ys = Y(a) 
                                       in let out ←─ xs + ys
                                          in <<X', Y'>, out>;XY.let X,Y = XY 
                                                             in hdf-halted(X) ∧b hdf-halted(Y);s1)
                    , b
                    >)*(v)) 
= hdf-halted(fst(X1 || X2 (hdfs1 + hdfs2) >>= X(u))*(v))
BY
{ ... }

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. hdfs2 : bag(hdataflow(A;C))@i
14. ¬((↑hdf-halted(X1 (hdfs1) >>= X)) ∧ (↑hdf-halted(X2 (hdfs2) >>= X)))
15. v2 : hdataflow(A;C)@i
16. v3 : bag(C)@i
17. fst(X1(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]) >>= X = v2 ∈ hdataflow(A;C)
18. ∪p∈bag-map(λP.P(u);hdfs1 + bag-map(X;snd(X1(u)))).snd(p) = v3 ∈ bag(C)
19. v5 : hdataflow(A;C)@i
20. v6 : bag(C)@i
21. fst(X2(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)]) >>= X = v5 ∈ hdataflow(A;C)
22. ∪p∈bag-map(λP.P(u);hdfs2 + bag-map(X;snd(X2(u)))).snd(p) = v6 ∈ bag(C)
⊢ hdf-halted(v2 || v5*(v)) 
= hdf-halted(fst(X1(u)) || fst(X2(u)) ([y∈bag-map(λP.(fst(P(u)));(hdfs1 + hdfs2)
                                          + bag-map(X;(snd(X1(u))) + (snd(X2(u)))))|¬bhdf-halted(y)]) >>= X*(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.  hdfs2  :  bag(hdataflow(A;C))@i
14.  \mneg{}((\muparrow{}hdf-halted(X1  (hdfs1)  >>=  X))  \mwedge{}  (\muparrow{}hdf-halted(X2  (hdfs2)  >>=  X)))
\mvdash{}  hdf-halted(fst(let  s1,b  =  let  X',xs  =  X1  (hdfs1)  >>=  X(u) 
                                                        in  let  Y',ys  =  X2  (hdfs2)  >>=  X(u) 
                                                              in  let  out  \mleftarrow{}{}  xs  +  ys
                                                                    in  <<X',  Y'>,  out> 
                                  in  <mk-hdf(XY,a.let  X,Y  =  XY 
                                                                  in  let  X',xs  =  X(a) 
                                                                        in  let  Y',ys  =  Y(a) 
                                                                              in  let  out  \mleftarrow{}{}  xs  +  ys
                                                                                    in  <<X',  Y'>,  out>XY.let  X,Y  =  XY 
                                                                                                                          in  hdf-halted(X)  \mwedge{}\msubb{}  hdf-halted(Y);s1)
                                        ,  b
                                        >)*(v)) 
=  hdf-halted(fst(X1  ||  X2  (hdfs1  +  hdfs2)  >>=  X(u))*(v))


By

---

Latex:
(((GenConclTerm  \mkleeneopen{}X1  (hdfs1)  >>=  X(u)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)
  THEN  (GenConclTerm  \mkleeneopen{}X2  (hdfs2)  >>=  X(u)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}v3  +  v6\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `hdf-parallel`  0
  THEN  (RWW  "hdf-bind-gen-ap  hdf-parallel-ap"  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  AllHyps  h.((RWO  "hdf-bind-gen-ap"  h  THEN  Auto)
                                  THEN  ((EqHD  h  THENM  (Reduce  h  THEN  Reduce  (h+1)))  THENA  Auto)
                                  )  )

---

Home Index