---

Step * of Lemma iterate-hdf-buffer2-simple

∀[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].
  ∀[L:A List]. ∀[a:A].  ((snd(hdf-buffer2(X;bs)*(L)(a))) = (snd(simple-hdf-buffer2(X;bs)*(L)(a))) ∈ bag(B)) 
  supposing valueall-type(B)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN Unfolds ``hdf-buffer2 simple-hdf-buffer2`` 0
   THEN RepeatFor 2 (MoveToConcl (-3))
   THEN ListInd (-1)
   THEN Auto
   THEN (HDataflowHD (-3) THENA Auto)
   THEN Reduce 0
   THEN RecUnfold `mk-hdf` 0
   THEN RepUR ``hdf-ap hdf-halted hdf-run hdf-halt`` 0
   THEN ((Fold `it` 0 THEN Fold `nil` 0 THEN Fold `empty-bag` 0)
   ORELSE (Fold `hdf-ap` 0 THEN Try (Fold `hdf-halted` 0))⋅
   )
   THEN Try (((GenApply (-1) THENA Auto)
              THEN D -2
              THEN Reduce 0
              THEN (CallByValueReduceOn ⌈∪f∈z2.bag-map(f;bs)⌉ 0⋅ THENA Auto)
              THEN Reduce 0
              THEN (BackThruSomeHyp⋅ ORELSE Auto))⋅)
   THEN Auto
   THEN Fold `hdf-halt` 0
   THEN (RWO "iterate-hdf-halt" 0 THENA Auto)
   THEN RW (AddrC [2] (BasicSymbolicComputeC [])) 0
   THEN Fold `it` 0
   THEN Fold `nil` 0
   THEN Fold `empty-bag` 0) }

1
1. A : Type
2. B : Type
3. valueall-type(B)
4. u : A
5. v : A List
6. ∀X:hdataflow(A;B ─→ B). ∀bs:bag(B). ∀a:A.
     ((snd(mk-hdf(Xbs,a.let X,bs = Xbs 
                        in let X',fs = X(a) 
                           in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                              in <<X', if bag-null(bs') then bs else bs' fi >, bs'>;s.let X,bs = s 
                                                                                   in hdf-halted(X);<X, bs>)*(v)(a)))
     = (snd(mk-hdf(Xbs,a.let X,bs = Xbs 
                         in let X',fs = X(a) 
                            in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                               in <<X', if bag-null(bs') then bs else bs' fi >, bs'>;s.ff;<X, bs>)*(v)(a)))
     ∈ bag(B))
7. bs : bag(B)@i
8. a : A@i
9. y : Unit@i
⊢ {}
= (snd(mk-hdf(Xbs,a.let X,bs = Xbs 
                    in let X',fs = X(a) 
                       in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                          in <<X', if bag-null(bs') then bs else bs' fi >, bs'>;s.ff;<hdf-halt(), bs>)*(v)(a)))
∈ bag(B)

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  B)].  \mforall{}[bs:bag(B)].
    \mforall{}[L:A  List].  \mforall{}[a:A].    ((snd(hdf-buffer2(X;bs)*(L)(a)))  =  (snd(simple-hdf-buffer2(X;bs)*(L)(a)))) 
    supposing  valueall-type(B)


By

(Auto
  THEN  MoveToConcl  (-1)
  THEN  Unfolds  ``hdf-buffer2  simple-hdf-buffer2``  0
  THEN  RepeatFor  2  (MoveToConcl  (-3))
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  (HDataflowHD  (-3)  THENA  Auto)
  THEN  Reduce  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  RepUR  ``hdf-ap  hdf-halted  hdf-run  hdf-halt``  0
  THEN  ((Fold  `it`  0  THEN  Fold  `nil`  0  THEN  Fold  `empty-bag`  0)
  ORELSE  (Fold  `hdf-ap`  0  THEN  Try  (Fold  `hdf-halted`  0))\mcdot{}
  )
  THEN  Try  (((GenApply  (-1)  THENA  Auto)
                        THEN  D  -2
                        THEN  Reduce  0
                        THEN  (CallByValueReduceOn  \mkleeneopen{}\mcup{}f\mmember{}z2.bag-map(f;bs)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  Reduce  0
                        THEN  (BackThruSomeHyp\mcdot{}  ORELSE  Auto))\mcdot{})
  THEN  Auto
  THEN  Fold  `hdf-halt`  0
  THEN  (RWO  "iterate-hdf-halt"  0  THENA  Auto)
  THEN  RW  (AddrC  [2]  (BasicSymbolicComputeC  []))  0
  THEN  Fold  `it`  0
  THEN  Fold  `nil`  0
  THEN  Fold  `empty-bag`  0)

---

Home Index