---

Step * 1 2 1 1 1 1 of Lemma iterate-hdf-bind-simple

.....equality..... 
1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. valueall-type(C)
6. X : hdataflow(A;B)@i
7. ys1 : bag(hdataflow(A;C))@i
8. ys2 : bag(hdataflow(A;C))@i
9. a : A@i
10. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
16. ∀[ba,bb:bag(hdataflow(A;C) × bag(C))]. ∀[f:(hdataflow(A;C) × bag(C)) ─→ bag(C)].
      (∪x∈ba + bb.f[x] = (∪x∈ba.f[x] + ∪x∈bb.f[x]) ∈ bag(C))
17. ([x∈ys2|hdf-halted(x)] + [x∈ys2|¬bhdf-halted(x)]) = ys2 ∈ bag(hdataflow(A;C))
⊢ ∪yb∈bag-map(λP.P(a);[x∈ys2|hdf-halted(x)]).snd(yb) ~ {}
BY
{ ((Using [`T',C] (BLemma `equal-empty-bag`)⋅ THENA Auto)
   THEN (InstLemma `bag-combine-map` [⌈hdataflow(A;C)⌉;⌈hdataflow(A;C) × bag(C)⌉;⌈C⌉]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto
   THEN (Reduce 0
         THEN GenConclAtAddr [2;1]
         THEN Assert ⌈∪yb∈v.{} = {} ∈ bag(C)⌉⋅
         THEN RWW "bag-combine-empty-right" 0
         THEN Auto
         THEN NthHypEq (-1)
         THEN RepeatFor 2 ((EqCD THEN Auto))
         THEN D (-1)
         THEN MoveToConcl (-1)
         THEN (HDataflowHD (-1) THENA Auto)
         THEN RepUR ``hdf-halted hdf-ap`` 0
         THEN Auto)⋅)⋅ }

---

Latex:


.....equality..... 
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  hdataflow(A;C)
5.  valueall-type(C)
6.  X  :  hdataflow(A;B)@i
7.  ys1  :  bag(hdataflow(A;C))@i
8.  ys2  :  bag(hdataflow(A;C))@i
9.  a  :  A@i
10.  ys1  =  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i
11.  (\mneg{}(ys1  =  \{\}))  \mvee{}  (\mneg{}\muparrow{}hdf-halted(X))
12.  v1  :  hdataflow(A;B)@i
13.  v2  :  bag(B)@i
14.  X(a)  =  <v1,  v2>@i
15.  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))
16.  \mforall{}[ba,bb:bag(hdataflow(A;C)  \mtimes{}  bag(C))].  \mforall{}[f:(hdataflow(A;C)  \mtimes{}  bag(C))  {}\mrightarrow{}  bag(C)].
            (\mcup{}x\mmember{}ba  +  bb.f[x]  =  (\mcup{}x\mmember{}ba.f[x]  +  \mcup{}x\mmember{}bb.f[x]))
17.  ([x\mmember{}ys2|hdf-halted(x)]  +  [x\mmember{}ys2|\mneg{}\msubb{}hdf-halted(x)])  =  ys2
\mvdash{}  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);[x\mmember{}ys2|hdf-halted(x)]).snd(yb)  \msim{}  \{\}


By

((Using  [`T',C]  (BLemma  `equal-empty-bag`)\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `bag-combine-map`  [\mkleeneopen{}hdataflow(A;C)\mkleeneclose{};\mkleeneopen{}hdataflow(A;C)  \mtimes{}  bag(C)\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  (Reduce  0
              THEN  GenConclAtAddr  [2;1]
              THEN  Assert  \mkleeneopen{}\mcup{}yb\mmember{}v.\{\}  =  \{\}\mkleeneclose{}\mcdot{}
              THEN  RWW  "bag-combine-empty-right"  0
              THEN  Auto
              THEN  NthHypEq  (-1)
              THEN  RepeatFor  2  ((EqCD  THEN  Auto))
              THEN  D  (-1)
              THEN  MoveToConcl  (-1)
              THEN  (HDataflowHD  (-1)  THENA  Auto)
              THEN  RepUR  ``hdf-halted  hdf-ap``  0
              THEN  Auto)\mcdot{})\mcdot{}

---

Home Index