---

Step * 1 1 of Lemma hdf-bind-gen-compose1-left


1. A : Type
2. B : Type
3. C : Type
4. U : Type
5. f : B ⟶ C
6. valueall-type(U)
7. valueall-type(C)
8. X : hdataflow(A;B)@i
9. Y : C ⟶ hdataflow(A;U)@i
10. hdfs : bag(hdataflow(A;U))@i
⊢ hdf-halted(f o X (hdfs) >>= Y) = hdf-halted(X (hdfs) >>= Y o f)
BY
{ (RepUR ``hdf-bind-gen hdf-compose1`` 0 THEN RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  U  :  Type
5.  f  :  B  {}\mrightarrow{}  C
6.  valueall-type(U)
7.  valueall-type(C)
8.  X  :  hdataflow(A;B)@i
9.  Y  :  C  {}\mrightarrow{}  hdataflow(A;U)@i
10.  hdfs  :  bag(hdataflow(A;U))@i
\mvdash{}  hdf-halted(f  o  X  (hdfs)  >>=  Y)  =  hdf-halted(X  (hdfs)  >>=  Y  o  f)


By

---

Latex:
(RepUR  ``hdf-bind-gen  hdf-compose1``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit))

---

Home Index