Step * 2 of Lemma length-nat-if-has-value


1. : ℤ
2. 0 < j
3. ∀l:Base
     ((λlist_ind,L. eval in
                    if is pair then let a,b 
                                        in (list_ind b) otherwise if Ax then otherwise ⊥^j 
       ⊥ 
       l)↓
      (fix((λlist_ind,L. eval in
                           if is pair then let a,b 
                                               in (list_ind b) otherwise if Ax then otherwise ⊥)) 
         l ∈ ℕ))
4. Base
5. (if Ax then otherwise ⊥)↓
6. (l)↓
7. ∀a,b:Top.  (if is pair then otherwise b)
⊢ fix((λlist_ind,L. eval in
                    if is pair then let a,b 
                                        in (list_ind b) otherwise if Ax then otherwise ⊥)) 
  l ∈ ℕ
BY
(HVimplies2 (-3) [1] THEN BotDiv THEN RW UnrollLoopsC THEN Reduce THEN Auto) }


Latex:


Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}l:Base
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  a,b  =  v 
                                                                              in  (list$_{ind}$  b)  +  1  otherwise  if  v  =  \000CAx  then  0  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              l)\mdownarrow{}
          {}\mRightarrow{}  (fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                    if  v  is  a  pair  then  let  a,b  =  v 
                                                                                            in  (list$_{ind}$  b)  +  1
                                                    otherwise  if  v  =  Ax  then  0  otherwise  \mbot{})) 
                  l  \mmember{}  \mBbbN{}))
4.  l  :  Base
5.  (if  l  =  Ax  then  0  otherwise  \mbot{})\mdownarrow{}
6.  (l)\mdownarrow{}
7.  \mforall{}a,b:Top.    (if  l  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  a,b  =  v 
                                                                              in  (list$_{ind}$  b)  +  1  otherwise  if  v  =  \000CAx  then  0  otherwise  \mbot{})) 
    l  \mmember{}  \mBbbN{}


By


Latex:
(HVimplies2  (-3)  [1]  THEN  BotDiv  THEN  RW  UnrollLoopsC  0  THEN  Reduce  0  THEN  Auto)




Home Index