---

Step * 1 of Lemma hdf-compose1-transformation2


1. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀f,L,G:Top.
     (λ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)\000C => inr ⋅ ^j - 1 ⊥ 
      fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))) 
      ≤ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                       λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
6. f : Top@i
7. L : Top@i
8. G : Top@i
⊢ inl (λa.let X',bs = cbva_seq(L a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))), G a g>; m) 
          in let out ⟵ bag-map(f;bs)
             in <λ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 ⋅ ^j - 1 
                 ⊥ 
                 X'
                , out
                >) ≤ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                                 λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1)))))
BY
{ (RW (AddrC [2] (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 (LiftAll 0 THENA Auto)
   THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
   THEN All (RepUR ``bag-map``)
   THEN BackThruSomeHyp)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(RW  (AddrC  [2]  (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  (LiftAll  0  THENA  Auto)
  THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  All  (RepUR  ``bag-map``)
  THEN  BackThruSomeHyp)\mcdot{}

---

Home Index