---

Step * 1 of Lemma has-value-length-member-list


1. j : ℤ
2. 0 < j
3. ∀l:Base
     ((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)↓
     ⇒ (λ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)↓
     ⇒ (l ∈ Base List))
4. l : Base@i
5. (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)↓
6. (eval v = l in
    if v is a pair then let a,b = v 
                        in (λ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 ⊥^\000Cj - 1 
                            ⊥ 
                            b)
                           + 1 otherwise if v = Ax then 0 otherwise ⊥)↓
7. ¬(j = 0 ∈ ℤ)
⊢ l ∈ Base List
BY
{ HasValueD (-2) }

1
1. j : ℤ
2. 0 < j
3. ∀l:Base
     ((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)↓
     ⇒ (λ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)↓
     ⇒ (l ∈ Base List))
4. l : Base@i
5. (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)↓
6. (if l is a pair then let a,b = l 
                        in (λ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 ⊥^\000Cj - 1 
                            ⊥ 
                            b)
                           + 1 otherwise if l = Ax then 0 otherwise ⊥)↓
7. ¬(j = 0 ∈ ℤ)
8. (l)↓
⊢ l ∈ Base List

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}l:Base
          ((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)\mdownarrow{}
          {}\mRightarrow{}  (\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  \000C=  Ax  then  0  otherwise  \mbot{}\^{}j  -  1 
                  \mbot{} 
                  l)\mdownarrow{}
          {}\mRightarrow{}  (l  \mmember{}  Base  List))
4.  l  :  Base@i
5.  (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  \000C=  Ax  then  0  otherwise  \mbot{})) 
        l)\mdownarrow{}
6.  (eval  v  =  l  in
        if  v  is  a  pair  then  let  a,b  =  v 
                                                in  (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                if  v  is  a  pair  then  let  a,b  =  v 
                                                                                                                        in  (list$_{ind}$  b)  \000C+  1
                                                                                otherwise  if  v  =  Ax  then  0  otherwise  \mbot{}\^{}j  -  1 
                                                        \mbot{} 
                                                        b)
                                                      +  1  otherwise  if  v  =  Ax  then  0  otherwise  \mbot{})\mdownarrow{}
7.  \mneg{}(j  =  0)
\mvdash{}  l  \mmember{}  Base  List


By

---

Latex:
HasValueD  (-2)

---

Home Index