---

Step * 2 of Lemma hdf-once-transformation3


1. j : ℤ
2. 0 < j
3. ∀L,G:Top. ∀m:ℕ. ∀a,g:Base.
     (case null(G a g)
       of inl() =>
       λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax , G a g>; m)))^j - 1 ⊥
       | inr() =>
       inr Ax  ≤ fix((λmk-hdf,s0. case s0
                                  of inl(y) =>
                                  inl (λa.let X',b = y a 
                                          in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                                  | inr(y) =>
                                  inr Ax )) 
                 case null(G a g)
                  of inl() =>
                  fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m)))))
                  | inr() =>
                  inr Ax )
4. L : Top@i
5. G : Top@i
6. m : ℕ@i
7. a : Base@i
8. g : Base@i
⊢ case null(G a g)
   of inl() =>
   inl (λa.cbva_seq(L a; λg.<case null(G a g)
                              of inl() =>
                              λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax 
                                                                , G a g
                                                                >; m)))^j - 1 
                              ⊥
                              | inr() =>
                              inr Ax 
                            , G a g
                            >; m))
   | inr() =>
   inr Ax  ≤ fix((λmk-hdf,s0. case s0
                              of inl(y) =>
                              inl (λa.let X',b = y a 
                                      in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                              | inr(y) =>
                              inr Ax )) 
             case null(G a g)
              of inl() =>
              fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m)))))
              | inr() =>
              inr Ax 
BY
{ (RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0 THEN (RWO "cbva_seq-spread" 0 THENA Auto) THEN Auto) }

---

Latex:



1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}L,G:Top.  \mforall{}m:\mBbbN{}.  \mforall{}a,g:Base.
          (case  null(G  a  g)
              of  inl()  =>
              \mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<case  null(G  a  g)  of  inl()  =>  mk-hdf  |  inr()  =>  inr  Ax 
                                                                                  ,  G  a  g
                                                                                  >  m)))\^{}j  -  1 
              \mbot{}
              |  inr()  =>
              inr  Ax    \mleq{}  fix((\mlambda{}mk-hdf,s0.  case  s0
                                                                    of  inl(y)  =>
                                                                    inl  (\mlambda{}a.let  X',b  =  y  a 
                                                                                    in  <mk-hdf  case  null(b)  of  inl()  =>  X'  |  inr()  =>  inr  Ax 
                                                                                          ,  b
                                                                                          >)
                                                                    |  inr(y)  =>
                                                                    inr  Ax  )) 
                                  case  null(G  a  g)
                                    of  inl()  =>
                                    fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<mk-hdf,  G  a  g>  m)))))
                                    |  inr()  =>
                                    inr  Ax  )
4.  L  :  Top@i
5.  G  :  Top@i
6.  m  :  \mBbbN{}@i
7.  a  :  Base@i
8.  g  :  Base@i
\mvdash{}  case  null(G  a  g)
      of  inl()  =>
      inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<case  null(G  a  g)
                                                            of  inl()  =>
                                                            \mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<case  null(G  a  g)
                                                                                                                                    of  inl()  =>
                                                                                                                                    mk-hdf
                                                                                                                                    |  inr()  =>
                                                                                                                                    inr  Ax 
                                                                                                                                ,  G  a  g
                                                                                                                                >  m)))\^{}j  -  1 
                                                            \mbot{}
                                                            |  inr()  =>
                                                            inr  Ax 
                                                        ,  G  a  g
                                                        >  m))
      |  inr()  =>
      inr  Ax    \mleq{}  fix((\mlambda{}mk-hdf,s0.  case  s0
                                                            of  inl(y)  =>
                                                            inl  (\mlambda{}a.let  X',b  =  y  a 
                                                                            in  <mk-hdf  case  null(b)  of  inl()  =>  X'  |  inr()  =>  inr  Ax  ,  b>)
                                                            |  inr(y)  =>
                                                            inr  Ax  )) 
                          case  null(G  a  g)
                            of  inl()  =>
                            fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L  a;  \mlambda{}g.<mk-hdf,  G  a  g>  m)))))
                            |  inr()  =>
                            inr  Ax 


By

(RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  Auto)

---

Home Index