---

Step * of Lemma hdf-bind-gen-ap-eq

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))]. ∀[a:A].
  X (hdfs) >>= Y(a)
  = <fst(X(a)) ([y∈bag-map(λP.(fst(P(a)));hdfs + bag-map(Y;snd(X(a))))|¬bhdf-halted(y)]) >>= Y
    , ∪p∈bag-map(λP.P(a);hdfs + bag-map(Y;snd(X(a)))).snd(p)
    >
  ∈ (hdataflow(A;C) × bag(C)) 
  supposing valueall-type(C)
BY
{ (Auto THEN RWO "hdf-bind-gen-ap<" 0 THEN Auto) }

---

Latex:


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


By

(Auto  THEN  RWO  "hdf-bind-gen-ap<"  0  THEN  Auto)

---

Home Index