---

Step * 2 of Lemma hdf-compose0-transformation1


1. f : Top
2. L : Top
3. m : ℕ
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀S,G,s:Top.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                   λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m + 1)))^j - 1 
      ⊥ 
      s ≤ fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ←─ ∪b∈bs.f b in <mk-hdf X', out>) | i\000Cnr(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))
8. S : Top@i
9. G : Top@i
10. s : Top@i
⊢ inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                   λg.<λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                                    λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m
                                                    + 1)))^j - 1 
                       ⊥ 
                       (S s a partial_ap(g;m + 1;m))
                      , select_fun_last(g;m)
                      >; m + 1)) ≤ fix((λmk-hdf,s0. case s0
                                                    of inl(y) =>
                                                    inl (λa.let X',bs = y a 
                                                            in let out ←─ ∪b∈bs.f b
                                                               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))))) s)
BY
{ (RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 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`` 0
   THEN (RW LiftAllC 0 THENA Auto)
   THEN Fold `select_fun_last` 0
   THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
   THEN BackThruSomeHyp) }

---

Latex:



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


By

(RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  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``  0
  THEN  (RW  LiftAllC  0  THENA  Auto)
  THEN  Fold  `select\_fun\_last`  0
  THEN  RepeatFor  3  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp)

---

Home Index