---

Step * of Lemma hdf-compose2-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B ─→ bag(C))]. ∀[Y:hdataflow(A;B)].
  ∀[a:A]. (X o Y(a) = <(fst(X(a))) o (fst(Y(a))), ∪f∈snd(X(a)).∪b∈snd(Y(a)).f b> ∈ (hdataflow(A;C) × bag(C))) 
  supposing valueall-type(C)
BY
{ (Auto
   THEN RepUR ``hdf-compose2 hdf-ap`` 0
   THEN RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
   THEN Reduce 0
   THEN Fold `hdf-ap` 0
   THEN Repeat (AutoSplit)
   THEN HDataflowHDAll
   THEN Try ((CallByValueReduceAtAddr [2;1] 0 THENA Auto))
   THEN Reduce 0
   THEN Try (Complete ((RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Auto)))
   THEN Fold `hdf-compose2` 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[Y:hdataflow(A;B)].
    \mforall{}[a:A].  (X  o  Y(a)  =  <(fst(X(a)))  o  (fst(Y(a))),  \mcup{}f\mmember{}snd(X(a)).\mcup{}b\mmember{}snd(Y(a)).f  b>) 
    supposing  valueall-type(C)


By

(Auto
  THEN  RepUR  ``hdf-compose2  hdf-ap``  0
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `mk-hdf`))  0
  THEN  Reduce  0
  THEN  Fold  `hdf-ap`  0
  THEN  Repeat  (AutoSplit)
  THEN  HDataflowHDAll
  THEN  Try  ((CallByValueReduceAtAddr  [2;1]  0  THENA  Auto))
  THEN  Reduce  0
  THEN  Try  (Complete  ((RecUnfold  `mk-hdf`  0  THEN  Reduce  0  THEN  Auto)))
  THEN  Fold  `hdf-compose2`  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index