---

Step * 2 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
11. a : A@i
⊢ hdf-out(f o X (hdfs) >>= Y;a) = hdf-out(X (hdfs) >>= Y o f;a) ∈ bag(U)
BY
{ (RepUR ``hdf-bind-gen hdf-compose1`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN (RWO "hdf-out-run" 0 THENA Auto)
   THEN RepUR ``bind-nxt`` 0
   THEN Fold `bind-nxt` 0
   THEN HDataflowHDAll⋅
   THEN (((CallByValueReduceAtAddr [2;1;1;1;1] 0 THENA Auto)
          THEN Reduce 0
          THEN (RWO "bag-map-map" 0 THENA Auto)
          THEN (GenConcl ⌜bag-map(λP.P(a);hdfs + bag-map(Y o f;z2)) = Z ∈ bag(hdataflow(A;U) × bag(U))⌝⋅ THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto))
   ORELSE ((GenConcl ⌜bag-map(λP.P(a);hdfs + {}) = Z ∈ bag(hdataflow(A;U) × bag(U))⌝⋅ THENA Auto)
           THEN (CallByValueReduce 0 THENA Auto)
           )
   )
   THEN ((GenConcl ⌜[y∈bag-map(λyb.(fst(yb));Z)|¬bhdf-halted(y)] = W ∈ bag(hdataflow(A;U))⌝⋅
          THENA (Try (BLemma `bag-filter-wf3`) THEN Auto)
          )⋅
         THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
         THEN Reduce 0
         THEN Auto)⋅) }

---

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
11.  a  :  A@i
\mvdash{}  hdf-out(f  o  X  (hdfs)  >>=  Y;a)  =  hdf-out(X  (hdfs)  >>=  Y  o  f;a)


By

---

Latex:
(RepUR  ``hdf-bind-gen  hdf-compose1``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  (RWO  "hdf-out-run"  0  THENA  Auto)
  THEN  RepUR  ``bind-nxt``  0
  THEN  Fold  `bind-nxt`  0
  THEN  HDataflowHDAll\mcdot{}
  THEN  (((CallByValueReduceAtAddr  [2;1;1;1;1]  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (RWO  "bag-map-map"  0  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}bag-map(\mlambda{}P.P(a);hdfs  +  bag-map(Y  o  f;z2))  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto))
  ORELSE  ((GenConcl  \mkleeneopen{}bag-map(\mlambda{}P.P(a);hdfs  +  \{\})  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  (CallByValueReduce  0  THENA  Auto)
                  )
  )
  THEN  ((GenConcl  \mkleeneopen{}[y\mmember{}bag-map(\mlambda{}yb.(fst(yb));Z)|\mneg{}\msubb{}hdf-halted(y)]  =  W\mkleeneclose{}\mcdot{}
                THENA  (Try  (BLemma  `bag-filter-wf3`)  THEN  Auto)
                )\mcdot{}
              THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index