---

Step * 1 2 2 1 1 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. 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)
23. ∀[p,as,bs:Top].  ([x∈as + bs|p[x]] ~ [x∈as|p[x]] + [x∈bs|p[x]])
⊢ [y∈bag-map(λP.(fst(P(u)));(hdfs1 + hdfs2) + bag-map(X;(snd(X1(u))) + (snd(X2(u)))))|¬bhdf-halted(y)]
= ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]
  + [y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)])
∈ bag(hdataflow(A;C))
BY
{ ((RWW "bag-map-append bag-filter-append" 0 THENA Auto)
   THEN GenConclAtAddr [2;1;1]
   THEN GenConclAtAddr [2;1;2]
   THEN GenConclAtAddr [2;2;1]
   THEN GenConclAtAddr [2;2;2]
   THEN All Thin) }

1
1. A : Type
2. C : Type
3. v7 : bag({y:hdataflow(A;C)| ↑¬bhdf-halted(y)} )@i
4. v8 : bag({y:hdataflow(A;C)| ↑¬bhdf-halted(y)} )@i
5. v9 : bag({y:hdataflow(A;C)| ↑¬bhdf-halted(y)} )@i
6. v10 : bag({y:hdataflow(A;C)| ↑¬bhdf-halted(y)} )@i
⊢ ((v7 + v8) + v9 + v10) = ((v7 + v9) + v8 + v10) ∈ bag(hdataflow(A;C))

---

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)))
15.  v2  :  hdataflow(A;C)@i
16.  v3  :  bag(C)@i
17.  fst(X1(u))  ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs1  +  bag-map(X;snd(X1(u))))|\mneg{}\msubb{}hdf-halted(y)])  >>=  X  =  v\000C2
18.  \mcup{}p\mmember{}bag-map(\mlambda{}P.P(u);hdfs1  +  bag-map(X;snd(X1(u)))).snd(p)  =  v3
19.  v5  :  hdataflow(A;C)@i
20.  v6  :  bag(C)@i
21.  fst(X2(u))  ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs2  +  bag-map(X;snd(X2(u))))|\mneg{}\msubb{}hdf-halted(y)])  >>=  X  =  v\000C5
22.  \mcup{}p\mmember{}bag-map(\mlambda{}P.P(u);hdfs2  +  bag-map(X;snd(X2(u)))).snd(p)  =  v6
23.  \mforall{}[p,as,bs:Top].    ([x\mmember{}as  +  bs|p[x]]  \msim{}  [x\mmember{}as|p[x]]  +  [x\mmember{}bs|p[x]])
\mvdash{}  [y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));(hdfs1  +  hdfs2)  +  bag-map(X;(snd(X1(u)))  +  (snd(X2(u)))))|
      \mneg{}\msubb{}hdf-halted(y)]
=  ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs1  +  bag-map(X;snd(X1(u))))|\mneg{}\msubb{}hdf-halted(y)]
    +  [y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs2  +  bag-map(X;snd(X2(u))))|\mneg{}\msubb{}hdf-halted(y)])


By

---

Latex:
((RWW  "bag-map-append  bag-filter-append"  0  THENA  Auto)
  THEN  GenConclAtAddr  [2;1;1]
  THEN  GenConclAtAddr  [2;1;2]
  THEN  GenConclAtAddr  [2;2;1]
  THEN  GenConclAtAddr  [2;2;2]
  THEN  All  Thin)

---

Home Index