---

Step * 1 of Lemma hdf-once-transformation2


1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,S,init: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 g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
       | inr() =>
       inr Ax  ≤ case null(G g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>;
                                         m))))) 
       (S g init)
       | inr() =>
       inr Ax )
5. L : Top@i
6. G : Top@i
7. S : Top@i
8. init : Top@i
9. m : ℕ@i
10. a : Base@i
11. g : Base@i
⊢ case case null(G g)
        of inl() =>
        fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
        | 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 g)
   of inl() =>
   fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>; m)))\000C)) 
   (S g init)
   | inr() =>
   inr Ax 
BY
{ (LiftAll 0
   THEN SqLeCD
   THEN Try (Complete (Auto))
   THEN (RW (AddrC [1;1] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0 THEN Reduce 0)
   THEN RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN RepeatFor 5 ((SqLeCD THEN Try (Complete (Auto))))
   THEN InstHyp [⌈L⌉;⌈G⌉;⌈S⌉;⌈S g init⌉;⌈m⌉;⌈a⌉;⌈g@0⌉] 4⋅
   THEN Auto)⋅ }

1
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,S,init: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 g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
       | inr() =>
       inr Ax  ≤ case null(G g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>;
                                         m))))) 
       (S g init)
       | inr() =>
       inr Ax )
5. L : Top@i
6. G : Top@i
7. S : Top@i
8. init : Top@i
9. m : ℕ@i
10. a : Base@i
11. g : Base@i
12. @0 : Base
13. a@0 : Base
14. g@0 : Base
15. λ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 g@0)
     of inl() =>
     fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g@0 (S g init))
     | inr() =>
     inr Ax  ≤ case null(G g@0)
     of inl() =>
     fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>;
                                       m))))) 
     (S g@0 (S g init))
     | inr() =>
     inr Ax 
⊢ λ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 g@0)
   of inl() =>
   inl (λa.cbva_seq(L (S g@0 (S g init)) a; λg@1.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>;
                                                                                    m))))) 
                                                  (S g@1 (S g@0 (S g init)))
                                                 , G g@1
                                                 >; m))
   | inr() =>
   inr Ax  ≤ case null(G g@0)
   of inl() =>
   fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>; m)))\000C)) 
   (S g@0 (S g init))
   | inr() =>
   inr Ax 

---

Latex:



1.  j  :  \mBbbZ{}
2.  j  \mneq{}  0
3.  0  <  j
4.  \mforall{}L,G,S,init: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  g)
              of  inl()  =>
              fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<mk-hdf  (S  g  s),  G  g>  m)))))  (S  g  init)
              |  inr()  =>
              inr  Ax    \mleq{}  case  null(G  g)
              of  inl()  =>
              fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<case  null(G  g)
                                                                                                          of  inl()  =>
                                                                                                          mk-hdf  (S  g  s)
                                                                                                          |  inr()  =>
                                                                                                          inr  Ax 
                                                                                                      ,  G  g
                                                                                                      >  m))))) 
              (S  g  init)
              |  inr()  =>
              inr  Ax  )
5.  L  :  Top@i
6.  G  :  Top@i
7.  S  :  Top@i
8.  init  :  Top@i
9.  m  :  \mBbbN{}@i
10.  a  :  Base@i
11.  g  :  Base@i
\mvdash{}  case  case  null(G  g)
                of  inl()  =>
                fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<mk-hdf  (S  g  s),  G  g>  m)))))  (S  g  init)
                |  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  g)
      of  inl()  =>
      fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L  s  a;  \mlambda{}g.<case  null(G  g)
                                                                                                  of  inl()  =>
                                                                                                  mk-hdf  (S  g  s)
                                                                                                  |  inr()  =>
                                                                                                  inr  Ax 
                                                                                              ,  G  g
                                                                                              >  m))))) 
      (S  g  init)
      |  inr()  =>
      inr  Ax 


By

(LiftAll  0
  THEN  SqLeCD
  THEN  Try  (Complete  (Auto))
  THEN  (RW  (AddrC  [1;1]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0  THEN  Reduce  0)
  THEN  RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  RepeatFor  5  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}S  g  init\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}g@0\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index