---

Step * 2 of Lemma hdf-buffer-transformation2


1. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀init,L,G:Top.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n);
                                   λg.<mk-hdf 
                                       case null(select_fun_last(g;m)) of inl() => s | inr() => select_fun_last(g;m)
                                      , select_fun_last(g;m)
                                      >; m + 1)))^j - 1 
      ⊥ 
      init ≤ fix((λmk-hdf,s0. let X,bs = s0 
                              in case X
                                  of inl(y) =>
                                  inl (λa.let X',fs = y a 
                                          in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                             in <mk-hdf <X', case null(bs') of inl() => bs | inr() => bs'>, bs'>)
                                  | inr(y) =>
                                  inr ⋅ )) 
             <fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>)
6. init : Top@i
7. L : Top@i
8. G : Top@i
⊢ inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈init.f b;m)  else (L a n);
                   λg.<λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n);
                                                    λg.<mk-hdf 
                                                        case null(select_fun_last(g;m))
                                                         of inl() =>
                                                         s
                                                         | inr() =>
                                                         select_fun_last(g;m)
                                                       , select_fun_last(g;m)
                                                       >; m + 1)))^j - 1 
                       ⊥ 
                       case null(select_fun_last(g;m)) of inl() => init | inr() => select_fun_last(g;m)
                      , select_fun_last(g;m)
                      >; m + 1)) ≤ fix((λmk-hdf,s0. let X,bs = s0 
                                                    in case X
                                                        of inl(y) =>
                                                        inl (λa.let X',fs = y a 
                                                                in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                                                   in <mk-hdf 
                                                                       <X'
                                                                       , case null(bs') of inl() => bs | inr() => bs'
                                                                       >
                                                                      , bs'
                                                                      >)
                                                        | inr(y) =>
                                                        inr ⋅ )) 
                                   <fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>
BY
{ (RW (AddrC [2;1] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
   THEN Reduce 0
   THEN RepeatFor 2 (SqLeCD)
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN (RWO "cbva_seq_extend" 0 THENA Auto)
   THEN RepUR ``ifthenelse eq_int btrue bfalse bag-map`` 0
   THEN RW LiftAllC 0
   THEN Fold `select_fun_last` 0
   THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
   THEN BackThruSomeHyp) }

---

Latex:



1.  m  :  \mBbbN{}
2.  j  :  \mBbbZ{}
3.  j  \mneq{}  0
4.  0  <  j
5.  \mforall{}init,L,G:Top.
          (\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  g.\mcup{}b\mmember{}s.f  b;m)
                                                                                  else  (L  a  n);  \mlambda{}g.<mk-hdf 
                                                                                                                      case  null(select\_fun\_last(g;m))
                                                                                                                        of  inl()  =>
                                                                                                                        s
                                                                                                                        |  inr()  =>
                                                                                                                        select\_fun\_last(g;m)
                                                                                                                    ,  select\_fun\_last(g;m)
                                                                                                                    >  m  +  1)))\^{}j  -  1 
            \mbot{} 
            init  \mleq{}  fix((\mlambda{}mk-hdf,s0.  let  X,bs  =  s0 
                                                            in  case  X
                                                                    of  inl(y)  =>
                                                                    inl  (\mlambda{}a.let  X',fs  =  y  a 
                                                                                    in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                                                                          in  <mk-hdf 
                                                                                                  <X',  case  null(bs')  of  inl()  =>  bs  |  inr()  =>  bs'>
                                                                                                ,  bs'
                                                                                                >)
                                                                    |  inr(y)  =>
                                                                    inr  \mcdot{}  )) 
                          <fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<mk-hdf,  G  g>  m))))),  init>)
6.  init  :  Top@i
7.  L  :  Top@i
8.  G  :  Top@i
\mvdash{}  inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m    then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  g.\mcup{}b\mmember{}init.f  b;m)    else  (L  a  n);
                                      \mlambda{}g.<\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                                                    then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  g.\mcup{}b\mmember{}s.f  b;m)
                                                                                                                    else  (L  a  n);
                                                                                                        \mlambda{}g.<mk-hdf 
                                                                                                                case  null(select\_fun\_last(g;m))
                                                                                                                  of  inl()  =>
                                                                                                                  s
                                                                                                                  |  inr()  =>
                                                                                                                  select\_fun\_last(g;m)
                                                                                                              ,  select\_fun\_last(g;m)
                                                                                                              >  m  +  1)))\^{}j  -  1 
                                              \mbot{} 
                                              case  null(select\_fun\_last(g;m))
                                                of  inl()  =>
                                                init
                                                |  inr()  =>
                                                select\_fun\_last(g;m)
                                            ,  select\_fun\_last(g;m)
                                            >  m  +  1))  \mleq{}  fix((\mlambda{}mk-hdf,s0.  let  X,bs  =  s0 
                                                                                                        in  case  X
                                                                                                                of  inl(y)  =>
                                                                                                                inl  (\mlambda{}a.let  X',fs  =  y  a 
                                                                                                                                in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                                                                                                                      in  <mk-hdf 
                                                                                                                                              <X'
                                                                                                                                              ,  case  null(bs')
                                                                                                                                                    of  inl()  =>
                                                                                                                                                    bs
                                                                                                                                                    |  inr()  =>
                                                                                                                                                    bs'
                                                                                                                                              >
                                                                                                                                            ,  bs'
                                                                                                                                            >)
                                                                                                                |  inr(y)  =>
                                                                                                                inr  \mcdot{}  )) 
                                                                      <fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<mk-hdf,  G  g>  m)))))
                                                                      ,  init
                                                                      >


By

(RW  (AddrC  [2;1]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (SqLeCD)
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  (RWO  "cbva\_seq\_extend"  0  THENA  Auto)
  THEN  RepUR  ``ifthenelse  eq\_int  btrue  bfalse  bag-map``  0
  THEN  RW  LiftAllC  0
  THEN  Fold  `select\_fun\_last`  0
  THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp)

---

Home Index