---

Step * 2 of Lemma hdf-state-transformation2


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

---

Latex:



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


By

(RW  (AddrC  [2;1]  UnrollLoopsC)  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  RepeatFor  2  ((RWO  "cbva\_seq\_extend"  0  THENA  Auto))
  THEN  RepUR  ``ifthenelse  eq\_int  btrue  bfalse  bag-map``  0
  THEN  (RW  (AddrC  [2;1]  LiftAllC)  0  THENA  Auto)
  THEN  All  (RepUR  ``bag-map  ifthenelse``)
  THEN  Fold  `select\_fun\_last`  0
  THEN  (Subst  \mkleeneopen{}(m  +  1)  +  1  \msim{}  m  +  2\mkleeneclose{}  0\mcdot{}  THENA  Auto')
  THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp)

---

Home Index