---

Step * of Lemma hdf-bind-gen-ap

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))]. ∀[a:A].
  X (hdfs) >>= Y(a) ~ <fst(X(a)) ([y∈bag-map(λP.(fst(P(a)));hdfs + bag-map(Y;snd(X(a))))|¬bhdf-halted(y)]) >>= Y
                      , ∪p∈bag-map(λP.P(a);hdfs + bag-map(Y;snd(X(a)))).snd(p)
                      > 
  supposing valueall-type(C)
BY
{ (Auto
   THEN RW (AddrC [1] (RepeatC (UnfoldsC ``hdf-bind-gen hdf-ap bind-nxt``))) 0
   THEN Fold `hdf-ap` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN (Try ((OnSomeHyp (\i.FLemma `hdf-halted-is-inr` [i] THENA Complete Auto)
               THEN HypSubst (-1) 0
               THEN Fold `hdf-halt` 0
               THEN Reduce 0)⋅)
         THEN Try (((FLemma `equal-empty-bag` [-2] THENA Auto)
                    THEN HypSubst (-1) 0
                    THEN (Reduce 0 THEN RWO "hdf-bind-gen-halt-left" 0 THEN Auto)⋅))
         )⋅
   THEN (RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `bind-nxt` 0
   THEN HDataflowHDAll
   THEN (Repeat (CallByValueReduceAtAddr [1;1] 0)
   THENM (Reduce 0
          THEN EqCD
          THEN Try (Complete (Auto))
          THEN Fold `hdf-bind-gen` 0
          THEN (RWO "bag-map-map" 0 THENA Auto)
          THEN RepUR ``compose`` 0
          THEN Auto)
   )
   THEN (GenConcl ⌈bag-map(λP.P(a);hdfs + bag-map(Y;z2)) = Z ∈ bag(hdataflow(A;C) × bag(C))⌉⋅
   ORELSE GenConcl ⌈bag-map(λP.P(a);hdfs + {}) = Z ∈ bag(hdataflow(A;C) × bag(C))⌉⋅
   )
   THEN Auto
   THEN (GenConcl ⌈[y∈bag-map(λyb.(fst(yb));Z)|¬bhdf-halted(y)] = W ∈ bag(hdataflow(A;C))⌉⋅
         THEN Auto
         THEN BLemma `bag-filter-wf3`
         THEN Auto)⋅) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[hdfs:bag(hdataflow(A;C))].  \mforall{}[a:A].
    X  (hdfs)  >>=  Y(a)  \msim{}  <fst(X(a))  ([y\mmember{}bag-map(\mlambda{}P.(fst(P(a)));hdfs  +  bag-map(Y;snd(X(a))))|
                                                                      \mneg{}\msubb{}hdf-halted(y)])  >>=  Y
                                            ,  \mcup{}p\mmember{}bag-map(\mlambda{}P.P(a);hdfs  +  bag-map(Y;snd(X(a)))).snd(p)
                                            > 
    supposing  valueall-type(C)


By

(Auto
  THEN  RW  (AddrC  [1]  (RepeatC  (UnfoldsC  ``hdf-bind-gen  hdf-ap  bind-nxt``)))  0
  THEN  Fold  `hdf-ap`  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  (Try  ((OnSomeHyp  (\mbackslash{}i.FLemma  `hdf-halted-is-inr`  [i]  THENA  Complete  Auto)
                          THEN  HypSubst  (-1)  0
                          THEN  Fold  `hdf-halt`  0
                          THEN  Reduce  0)\mcdot{})
              THEN  Try  (((FLemma  `equal-empty-bag`  [-2]  THENA  Auto)
                                    THEN  HypSubst  (-1)  0
                                    THEN  (Reduce  0  THEN  RWO  "hdf-bind-gen-halt-left"  0  THEN  Auto)\mcdot{}))
              )\mcdot{}
  THEN  (RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `bind-nxt`  0
  THEN  HDataflowHDAll
  THEN  (Repeat  (CallByValueReduceAtAddr  [1;1]  0)
  THENM  (Reduce  0
                THEN  EqCD
                THEN  Try  (Complete  (Auto))
                THEN  Fold  `hdf-bind-gen`  0
                THEN  (RWO  "bag-map-map"  0  THENA  Auto)
                THEN  RepUR  ``compose``  0
                THEN  Auto)
  )
  THEN  (GenConcl  \mkleeneopen{}bag-map(\mlambda{}P.P(a);hdfs  +  bag-map(Y;z2))  =  Z\mkleeneclose{}\mcdot{}
  ORELSE  GenConcl  \mkleeneopen{}bag-map(\mlambda{}P.P(a);hdfs  +  \{\})  =  Z\mkleeneclose{}\mcdot{}
  )
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}[y\mmember{}bag-map(\mlambda{}yb.(fst(yb));Z)|\mneg{}\msubb{}hdf-halted(y)]  =  W\mkleeneclose{}\mcdot{}
              THEN  Auto
              THEN  BLemma  `bag-filter-wf3`
              THEN  Auto)\mcdot{})

---

Home Index