---

Step * 1 of Lemma iterate-hdf-buffer-simple


1. A : Type
2. B : Type
3. valueall-type(B)
4. u : A
5. v : A List
6. ∀X:hdataflow(A;B ─→ bag(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.∪b∈bs.f b
                              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.∪b∈bs.f b
                               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
⊢ Ax
= (snd(mk-hdf(Xbs,a.let X,bs = Xbs 
                    in let X',fs = X(a) 
                       in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                          in <<X', if bag-null(bs') then bs else bs' fi >, bs'>;s.ff;<hdf-halt(), bs>)*(v)(a)))
∈ bag(B)
BY
{ (All Thin
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Auto
   THEN Reduce 0
   THEN RecUnfold `mk-hdf` 0
   THEN RepUR ``hdf-ap hdf-halt hdf-run`` 0
   THEN Auto
   THEN Try ((Fold `hdf-ap` 0 THEN Fold `hdf-halt` 0 THEN BackThruSomeHyp)⋅)) }

1
1. A : Type
2. B : Type
3. bs : bag(B)@i
4. a : A@i
⊢ Ax ∈ bag(B)

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  valueall-type(B)
4.  u  :  A
5.  v  :  A  List
6.  \mforall{}X:hdataflow(A;B  {}\mrightarrow{}  bag(B)).  \mforall{}bs:bag(B).  \mforall{}a:A.
          ((snd(mk-hdf(Xbs,a.let  X,bs  =  Xbs 
                                                in  let  X',fs  =  X(a) 
                                                      in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                                            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'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                                              in  <<X',  if  bag-null(bs')  then  bs  else  bs'  fi  >,  bs'>s.ff;<X,  bs>)*(\000Cv)(a))))
7.  bs  :  bag(B)@i
8.  a  :  A@i
9.  y  :  Unit@i
\mvdash{}  Ax
=  (snd(mk-hdf(Xbs,a.let  X,bs  =  Xbs 
                                        in  let  X',fs  =  X(a) 
                                              in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                                    in  <<X',  if  bag-null(bs')  then  bs  else  bs'  fi  >,  bs'>s.ff;<hdf-halt(),  bs\000C>)*(v)(a)))


By

(All  Thin
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  Reduce  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  RepUR  ``hdf-ap  hdf-halt  hdf-run``  0
  THEN  Auto
  THEN  Try  ((Fold  `hdf-ap`  0  THEN  Fold  `hdf-halt`  0  THEN  BackThruSomeHyp)\mcdot{}))

---

Home Index