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