Step
*
1
1
of Lemma
hdf-bind-gen-left-halt
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. Y : B ─→ hdataflow(A;C)@i
6. hdfs : bag(hdataflow(A;C))@i
⊢ hdf-halted(hdf-halt() (hdfs) >>= Y) = hdf-halted(hdf-halt() (hdfs) >>= λx.hdf-return({x}))
BY
{ (RepUR ``hdf-bind-gen bind-nxt`` 0 THEN RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Repeat (AutoSplit⋅)) }
Latex:
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. Y : B {}\mrightarrow{} hdataflow(A;C)@i
6. hdfs : bag(hdataflow(A;C))@i
\mvdash{} hdf-halted(hdf-halt() (hdfs) >>= Y) = hdf-halted(hdf-halt() (hdfs) >>= \mlambda{}x.hdf-return(\{x\}))
By
(RepUR ``hdf-bind-gen bind-nxt`` 0 THEN RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Repeat (AutoSplit\mcdot{}))
Home
Index