---

Step * 1 1 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
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) ~ λ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
BY
{ (EqCD THEN Try (Trivial)) }

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 
⊢ j + (-1) ~ j - 1

---

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
12.  @0  :  Base
13.  a@0  :  Base
14.  g@0  :  Base
15.  \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@0)
          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@0  (S  g  init))
          |  inr()  =>
          inr  Ax    \mleq{}  case  null(G  g@0)
          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@0  (S  g  init))
          |  inr()  =>
          inr  Ax 
\mvdash{}  \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)  \msim{}  \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


By

(EqCD  THEN  Try  (Trivial))

---

Home Index