---

Step * 2 of Lemma hdf-once-transformation2


1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,S,init:Top. ∀m:ℕ. ∀a,g:Base.
     (case null(G g)
       of inl() =>
       λ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)))^\000Cj - 1 ⊥ 
       (S g init)
       | 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 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 )
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 null(G g)
   of inl() =>
   inl (λa.cbva_seq(L (S g init) a; λg@0.<case null(G g@0)
                                           of inl() =>
                                           λ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)))^j - 1 
                                           ⊥ 
                                           (S g@0 (S g init))
                                           | inr() =>
                                           inr Ax 
                                         , G g@0
                                         >; 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 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 
BY
{ (RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN RepeatFor 6 ((SqLeCD THEN Try (Complete (Auto))))
   THEN InstHyp [⌈L⌉;⌈G⌉;⌈S⌉;⌈S g init⌉;⌈m⌉;⌈a⌉;⌈g@0⌉] 4⋅
   THEN Auto)⋅ }

---

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.
          (case  null(G  g)
              of  inl()  =>
              \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)))\^{}j  -  1 
              \mbot{} 
              (S  g  init)
              |  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  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  ini\000Ct)
                                    |  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  null(G  g)
      of  inl()  =>
      inl  (\mlambda{}a.cbva\_seq(L  (S  g  init)  a;  \mlambda{}g@0.<case  null(G  g@0)
                                                                                      of  inl()  =>
                                                                                      \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)))\^{}j  -  1 
                                                                                      \mbot{} 
                                                                                      (S  g@0  (S  g  init))
                                                                                      |  inr()  =>
                                                                                      inr  Ax 
                                                                                  ,  G  g@0
                                                                                  >  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  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 


By

(RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  RepeatFor  6  ((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