---

Step * 2 of Lemma hdf-buffer-transformation3


1. j : ℤ
2. 0 < j
3. ∀init,s,L,S,G:Top. ∀m:ℕ.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                         then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                         else (L (fst(s)) a n); λg.<mk-hdf 
                                                                    <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                    , case null(select_fun_last(g;m))
                                                                       of inl() =>
                                                                       snd(s)
                                                                       | inr() =>
                                                                       select_fun_last(g;m)
                                                                    >
                                                                   , select_fun_last(g;m)
                                                                   >; m + 1)))^j - 1 
      ⊥ 
      <s, 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init>)
4. init : Top@i
5. s : Top@i
6. L : Top@i
7. S : Top@i
8. G : Top@i
9. m : ℕ@i
⊢ (λx.((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                           then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                           else (L (fst(s)) a n); λg.<mk-hdf 
                                                                      <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                      , case null(select_fun_last(g;m))
                                                                         of inl() =>
                                                                         snd(s)
                                                                         | inr() =>
                                                                         select_fun_last(g;m)
                                                                      >
                                                                     , select_fun_last(g;m)
                                                                     >; m + 1)))) 
       (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                           then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                           else (L (fst(s)) a n); λg.<mk-hdf 
                                                                      <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                      , case null(select_fun_last(g;m))
                                                                         of inl() =>
                                                                         snd(s)
                                                                         | inr() =>
                                                                         select_fun_last(g;m)
                                                                      >
                                                                     , select_fun_last(g;m)
                                                                     >; m + 1)))^j - 1 
        x))) 
  ⊥ 
  <s, 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init>
BY
{ (RW (AddrC [2;1] (UnrollLoopsOnceExceptC (``pi1 pi2`` @ 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.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}init,s,L,S,G:Top.  \mforall{}m:\mBbbN{}.
          (\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  (fst(s))  a  g.\mcup{}b\mmember{}snd(s).f  b;m)
                                                                                  else  (L  (fst(s))  a  n);
                                                                      \mlambda{}g.<mk-hdf 
                                                                              <S  (fst(s))  a  partial\_ap(g;m  +  1;m)
                                                                              ,  case  null(select\_fun\_last(g;m))
                                                                                    of  inl()  =>
                                                                                    snd(s)
                                                                                    |  inr()  =>
                                                                                    select\_fun\_last(g;m)
                                                                              >
                                                                            ,  select\_fun\_last(g;m)
                                                                            >  m  +  1)))\^{}j  -  1 
            \mbot{} 
            <s,  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,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<mk-hdf  (S  s  a  g),  G  s  a  g>  m)))))  s\000C,  init>)
4.  init  :  Top@i
5.  s  :  Top@i
6.  L  :  Top@i
7.  S  :  Top@i
8.  G  :  Top@i
9.  m  :  \mBbbN{}@i
\mvdash{}  (\mlambda{}x.((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                      then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  (fst(s))  a  g.\mcup{}b\mmember{}snd(s).f  b;m)
                                                                                      else  (L  (fst(s))  a  n);
                                                                          \mlambda{}g.<mk-hdf 
                                                                                  <S  (fst(s))  a  partial\_ap(g;m  +  1;m)
                                                                                  ,  case  null(select\_fun\_last(g;m))
                                                                                        of  inl()  =>
                                                                                        snd(s)
                                                                                        |  inr()  =>
                                                                                        select\_fun\_last(g;m)
                                                                                  >
                                                                                ,  select\_fun\_last(g;m)
                                                                                >  m  +  1)))) 
              (\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                      then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G  (fst(s))  a  g.\mcup{}b\mmember{}snd(s).f  b;m)
                                                                                      else  (L  (fst(s))  a  n);
                                                                          \mlambda{}g.<mk-hdf 
                                                                                  <S  (fst(s))  a  partial\_ap(g;m  +  1;m)
                                                                                  ,  case  null(select\_fun\_last(g;m))
                                                                                        of  inl()  =>
                                                                                        snd(s)
                                                                                        |  inr()  =>
                                                                                        select\_fun\_last(g;m)
                                                                                  >
                                                                                ,  select\_fun\_last(g;m)
                                                                                >  m  +  1)))\^{}j  -  1 
                x))) 
    \mbot{} 
    <s,  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,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<mk-hdf  (S  s  a  g),  G  s  a  g>  m)))))  s,  in\000Cit>


By

(RW  (AddrC  [2;1]  (UnrollLoopsOnceExceptC  (``pi1  pi2``  @  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