---

Step * 1 of Lemma hdf-once-transformation3


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

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}L,G:Top.  \mforall{}m:\mBbbN{}.  \mforall{}a,g:Base.
          (\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  \^{}j  -  1 
            \mbot{} 
            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    \mleq{}  case  null(G  a  g)
              of  inl()  =>
              fix((\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)))))
              |  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  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 
      of  inl(y)  =>
      inl  (\mlambda{}a.let  X',b  =  y  a 
                      in  <\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  \^{}j  -  1 
                              \mbot{} 
                              case  null(b)  of  inl()  =>  X'  |  inr()  =>  inr  Ax 
                            ,  b
                            >)
      |  inr(y)  =>
      inr  Ax    \mleq{}  case  null(G  a  g)
      of  inl()  =>
      fix((\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)))))
      |  inr()  =>
      inr  Ax 


By

---

Latex:
(LiftRedAll
  THEN  SqLeCD
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  Auto)

---

Home Index