---

Step * 2 of Lemma has-value-l-last-default-list


1. j : ℤ
2. 0 < j
3. ∀l,d:Base.
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let h,t = v 
                                        in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
       ⊥ 
       l 
       d)↓
     ⇒ (l ∈ Top List))
4. l : Base@i
5. d : Base@i
6. (eval v = l in
    if v is a pair then let h,t = v 
                        in λx.(λlist_ind,L. eval v = L in
                                            if v is a pair then let h,t = v 
                                                                in λx.(list_ind t h)
                                            otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
                               ⊥ 
                               t 
                               h) otherwise if v = Ax then λx.x otherwise ⊥ 
    d)↓@i
7. (if l = Ax then λx.x otherwise ⊥)↓
8. (l)↓
9. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
⊢ l ∈ Top List
BY
{ HVimplies2 (-3) [1] }

1
1. j : ℤ
2. 0 < j
3. ∀l,d:Base.
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let h,t = v 
                                        in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
       ⊥ 
       l 
       d)↓
     ⇒ (l ∈ Top List))
4. l : Base@i
5. d : Base@i
6. (eval v = l in
    if v is a pair then let h,t = v 
                        in λx.(λlist_ind,L. eval v = L in
                                            if v is a pair then let h,t = v 
                                                                in λx.(list_ind t h)
                                            otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
                               ⊥ 
                               t 
                               h) otherwise if v = Ax then λx.x otherwise ⊥ 
    d)↓@i
7. (⊥)↓
8. (l)↓
9. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
10. ∀a,b:Top.  (if l = Ax then a otherwise b ~ b)
⊢ l ∈ Top List

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}l,d:Base.
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                              in  \mlambda{}x.(list$_{ind}$  t  h)  otherwise  if  v  =\000C  Ax  then  \mlambda{}x.x  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              l 
              d)\mdownarrow{}
          {}\mRightarrow{}  (l  \mmember{}  Top  List))
4.  l  :  Base@i
5.  d  :  Base@i
6.  (eval  v  =  l  in
        if  v  is  a  pair  then  let  h,t  =  v 
                                                in  \mlambda{}x.(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                              in  \mlambda{}x.(list$_{ind}\mbackslash{}ff\000C24  t  h)
                                                                                      otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{}\^{}j  -  1 
                                                              \mbot{} 
                                                              t 
                                                              h)  otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{} 
        d)\mdownarrow{}@i
7.  (if  l  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{})\mdownarrow{}
8.  (l)\mdownarrow{}
9.  \mforall{}a,b:Top.    (if  l  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  l  \mmember{}  Top  List


By

---

Latex:
HVimplies2  (-3)  [1]

---

Home Index