---

Step * of Lemma hdf-bind-gen-left-halt

∀[A,B,C:Type]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))].
  hdf-halt() (hdfs) >>= Y = hdf-halt() (hdfs) >>= λx.hdf-return({x}) ∈ hdataflow(A;C) supposing valueall-type(C)
BY
{ (Auto THEN BLemma `hdataflow-equal` THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. hdfs : bag(hdataflow(A;C))
6. valueall-type(C)
7. inputs : A List
⊢ hdf-halted(hdf-halt() (hdfs) >>= Y*(inputs)) = hdf-halted(hdf-halt() (hdfs) >>= λx.hdf-return({x})*(inputs))

2
1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. hdfs : bag(hdataflow(A;C))
6. valueall-type(C)
7. inputs : A List
8. hdf-halted(hdf-halt() (hdfs) >>= Y*(inputs)) = hdf-halted(hdf-halt() (hdfs) >>= λx.hdf-return({x})*(inputs))
9. a : A
⊢ hdf-out(hdf-halt() (hdfs) >>= Y*(inputs);a) = hdf-out(hdf-halt() (hdfs) >>= λx.hdf-return({x})*(inputs);a) ∈ bag(C)

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[hdfs:bag(hdataflow(A;C))].
    hdf-halt()  (hdfs)  >>=  Y  =  hdf-halt()  (hdfs)  >>=  \mlambda{}x.hdf-return(\{x\})  supposing  valueall-type(C)


By

(Auto  THEN  BLemma  `hdataflow-equal`  THEN  Auto)

---

Home Index