---

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


1. j : ℤ
2. 0 < j
3. ∀l:Base
     ((λ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 ⊥^j - 1 
       ⊥ 
       l)↓
     ⇒ (fix((λ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 ⊥)) 
         l ∈ ℕ))
4. l : Base
5. ((λ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 ⊥^j - 1 
     ⊥ 
     (snd(l)))
+ 1)↓
6. 0 ≤ 0
7. l ~ <fst(l), snd(l)>
⊢ fix((λ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 ⊥)) 
  <fst(l), snd(l)> ∈ ℕ
BY
{ (RW UnrollLoopsC 0 THEN Reduce 0 THEN HasValueD (-3) THEN GenerateHasValue [2] (-2) THEN FHyp (-8) [-1] 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.  ((\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\000C  then  0  otherwise  \mbot{}\^{}j  -  1 
          \mbot{} 
          (snd(l)))
+  1)\mdownarrow{}
6.  0  \mleq{}  0
7.  l  \msim{}  <fst(l),  snd(l)>
\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{})) 
    <fst(l),  snd(l)>  \mmember{}  \mBbbN{}


By

---

Latex:
(RW  UnrollLoopsC  0
  THEN  Reduce  0
  THEN  HasValueD  (-3)
  THEN  GenerateHasValue  [2]  (-2)
  THEN  FHyp  (-8)  [-1]
  THEN  Auto)

---

Home Index