---

Step * of Lemma hdf-bind-gen-halted

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))].
  hdf-halted(X (hdfs) >>= Y) = hdf-halted(X) ∧b bag-null(hdfs) supposing valueall-type(C)
BY
{ (Auto
   THEN RepUR ``hdf-halted hdf-bind-gen`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Fold `hdf-halted` 0
   THEN BoolCase ⌈hdf-halted(X) ∧b bag-null(hdfs)⌉⋅
   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))].
    hdf-halted(X  (hdfs)  >>=  Y)  =  hdf-halted(X)  \mwedge{}\msubb{}  bag-null(hdfs)  supposing  valueall-type(C)


By

(Auto
  THEN  RepUR  ``hdf-halted  hdf-bind-gen``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Fold  `hdf-halted`  0
  THEN  BoolCase  \mkleeneopen{}hdf-halted(X)  \mwedge{}\msubb{}  bag-null(hdfs)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index