---

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

∀[A,B,C,U:Type]. ∀[f:B ─→ C]. ∀[X:hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;U)]. ∀[hdfs:bag(hdataflow(A;U))].
  (f o X (hdfs) >>= Y = X (hdfs) >>= Y o f ∈ hdataflow(A;U)) supposing (valueall-type(C) and valueall-type(U))
BY
{ (Auto THEN BLemma `hdataflow-equal` THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. U : Type
5. f : B ─→ C
6. X : hdataflow(A;B)
7. Y : C ─→ hdataflow(A;U)
8. hdfs : bag(hdataflow(A;U))
9. valueall-type(U)
10. valueall-type(C)
11. inputs : A List
⊢ hdf-halted(f o X (hdfs) >>= Y*(inputs)) = hdf-halted(X (hdfs) >>= Y o f*(inputs))

2
1. A : Type
2. B : Type
3. C : Type
4. U : Type
5. f : B ─→ C
6. X : hdataflow(A;B)
7. Y : C ─→ hdataflow(A;U)
8. hdfs : bag(hdataflow(A;U))
9. valueall-type(U)
10. valueall-type(C)
11. inputs : A List
12. hdf-halted(f o X (hdfs) >>= Y*(inputs)) = hdf-halted(X (hdfs) >>= Y o f*(inputs))
13. a : A
⊢ hdf-out(f o X (hdfs) >>= Y*(inputs);a) = hdf-out(X (hdfs) >>= Y o f*(inputs);a) ∈ bag(U)

---

Latex:


\mforall{}[A,B,C,U:Type].  \mforall{}[f:B  {}\mrightarrow{}  C].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:C  {}\mrightarrow{}  hdataflow(A;U)].
\mforall{}[hdfs:bag(hdataflow(A;U))].
    (f  o  X  (hdfs)  >>=  Y  =  X  (hdfs)  >>=  Y  o  f)  supposing  (valueall-type(C)  and  valueall-type(U))


By

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

---

Home Index