---

Step * 2 of Lemma hdf-compose1-transformation3


1. j : ℤ
2. 0 < j
3. ∀f,L,S,G,init:Top. ∀m:ℕ.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                   λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1 
      ⊥ 
      init ≤ fix((λmk-hdf,s0. case s0
                              of inl(y) =>
                              inl (λa.let X',bs = y a 
                                      in let out ⟵ bag-map(f;bs)
                                         in <mk-hdf X', out>)
                              | 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))))) init))
4. f : Top@i
5. L : Top@i
6. S : Top@i
7. G : Top@i
8. init : Top@i
9. m : ℕ@i
⊢ (λx.((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                     λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))) 
       (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                     λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1\000C 
        x))) 
  ⊥ 
  init ≤ fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ⟵ bag-map(f;bs) in <mk-hdf X', out>) \000C| 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))))) 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 THENA Auto)
   THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
   THEN All (RepUR ``bag-map``)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}f,L,S,G,init:Top.  \mforall{}m:\mBbbN{}.
          (\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.bag-map(f;G  s  a  g);m)
                                                                                  else  (L  s  a  n);  \mlambda{}g.<mk-hdf  (S  s  a  partial\_ap(g;m  +  1;m))
                                                                                                                        ,  select\_fun\_ap(g;m  +  1;m)
                                                                                                                        >  m  +  1)))\^{}j  -  1 
            \mbot{} 
            init  \mleq{}  fix((\mlambda{}mk-hdf,s0.  case  s0
                                                            of  inl(y)  =>
                                                            inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                                            in  let  out  \mleftarrow{}{}  bag-map(f;bs)
                                                                                  in  <mk-hdf  X',  out>)
                                                            |  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)))))  init))
4.  f  :  Top@i
5.  L  :  Top@i
6.  S  :  Top@i
7.  G  :  Top@i
8.  init  :  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.bag-map(f;G  s  a  g);m)
                                                                                      else  (L  s  a  n);  \mlambda{}g.<mk-hdf  (S  s  a  partial\_ap(g;m  +  1;m))
                                                                                                                            ,  select\_fun\_ap(g;m  +  1;m)
                                                                                                                            >  m  +  1)))) 
              (\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n=m
                                                                                      then  mk\_lambdas\_fun(\mlambda{}g.bag-map(f;G  s  a  g);m)
                                                                                      else  (L  s  a  n);  \mlambda{}g.<mk-hdf  (S  s  a  partial\_ap(g;m  +  1;m))
                                                                                                                            ,  select\_fun\_ap(g;m  +  1;m)
                                                                                                                            >  m  +  1)))\^{}j  -  1 
                x))) 
    \mbot{} 
    init  \mleq{}  fix((\mlambda{}mk-hdf,s0.  case  s0
                                                    of  inl(y)  =>
                                                    inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                                    in  let  out  \mleftarrow{}{}  bag-map(f;bs)
                                                                          in  <mk-hdf  X',  out>)
                                                    |  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)))))  init)


By

---

Latex:
(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  THENA  Auto)
  THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  All  (RepUR  ``bag-map``)
  THEN  BackThruSomeHyp)

---

Home Index