---

Step * of Lemma hdf-bind-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ⟶ hdataflow(A;C)]. ∀[a:A].
  X >>= Y(a)
  = <fst(X(a)) ([y∈bag-map(λx.(fst(Y x(a)));snd(X(a)))|¬bhdf-halted(y)]) >>= Y, ⋃p∈bag-map(λx.Y x(a);snd(X(a))).snd(p)>
  ∈ (hdataflow(A;C) × bag(C)) 
  supposing valueall-type(C)
BY
{ (Auto
   THEN (RWO "hdf-bind-as-gen" 0 THENA Auto)
   THEN (RWO "hdf-bind-gen-ap" 0 THEN Auto)
   THEN Reduce 0
   THEN (RWO "bag-map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[a:A].
    X  >>=  Y(a)
    =  <fst(X(a))  ([y\mmember{}bag-map(\mlambda{}x.(fst(Y  x(a)));snd(X(a)))|\mneg{}\msubb{}hdf-halted(y)])  >>=  Y
        ,  \mcup{}p\mmember{}bag-map(\mlambda{}x.Y  x(a);snd(X(a))).snd(p)
        > 
    supposing  valueall-type(C)


By

---

Latex:
(Auto
  THEN  (RWO  "hdf-bind-as-gen"  0  THENA  Auto)
  THEN  (RWO  "hdf-bind-gen-ap"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  (RWO  "bag-map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index