---

Step * 1 of Lemma islist-implies-is-list


1. j : ℤ
2. 0 < j
3. ∀t:Base
     ((λlist_ind,L. eval v = L in if v is a pair then let h,t = v in eval s = list_ind t in <h, s> otherwise if v = Ax t\000Chen [] otherwise ⊥^j - 1 ⊥ t)↓
     ⇒ (t ∈ Base List))
4. t : Base
5. (eval v = t in
    if v is a pair then let h,t = v 
                        in eval s = λlist_ind,L. eval v = L in
                                                 if v is a pair then let h,t = v 
                                                                     in eval s = list_ind t in
                                                                        <h, s> otherwise if v = Ax then [] otherwise ⊥^j\000C - 1 
                                    ⊥ 
                                    t in
                           <h, s> otherwise if v = Ax then [] otherwise ⊥)↓
6. ¬(j = 0 ∈ ℤ)
⊢ t ∈ Base List
BY
{ xxx(HasValueD (-2) THEN HVimplies2 (-3) [1] )xxx }

1
1. j : ℤ
2. 0 < j
3. ∀t:Base
     ((λlist_ind,L. eval v = L in if v is a pair then let h,t = v in eval s = list_ind t in <h, s> otherwise if v = Ax t\000Chen [] otherwise ⊥^j - 1 ⊥ t)↓
     ⇒ (t ∈ Base List))
4. t : Base
5. (eval s = λlist_ind,L. eval v = L in
                          if v is a pair then let h,t = v 
                                              in eval s = list_ind t in
                                                 <h, s> otherwise if v = Ax then [] otherwise ⊥^j - 1 
             ⊥ 
             (snd(t)) in
    <fst(t), s>)↓
6. ¬(j = 0 ∈ ℤ)
7. 0 ≤ 0
8. t ~ <fst(t), snd(t)>
⊢ <fst(t), snd(t)> ∈ Base List

2
1. j : ℤ
2. 0 < j
3. ∀t:Base
     ((λlist_ind,L. eval v = L in if v is a pair then let h,t = v in eval s = list_ind t in <h, s> otherwise if v = Ax t\000Chen [] otherwise ⊥^j - 1 ⊥ t)↓
     ⇒ (t ∈ Base List))
4. t : Base
5. (if t = Ax then [] otherwise ⊥)↓
6. ¬(j = 0 ∈ ℤ)
7. (t)↓
8. ∀a,b:Top.  (if t is a pair then a otherwise b ~ b)
⊢ t ∈ Base List

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}t:Base
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                              in  eval  s  =  list$_{ind}$  t  in
                                                                                    <h,  s>  otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              t)\mdownarrow{}
          {}\mRightarrow{}  (t  \mmember{}  Base  List))
4.  t  :  Base
5.  (eval  v  =  t  in
        if  v  is  a  pair  then  let  h,t  =  v 
                                                in  eval  s  =  \mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                                if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                                        in  eval  s  =  list$_{i\000Cnd}$  t  in
                                                                                                                                              <h,  s>
                                                                                                otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                                                                        \mbot{} 
                                                                        t  in
                                                      <h,  s>  otherwise  if  v  =  Ax  then  []  otherwise  \mbot{})\mdownarrow{}
6.  \mneg{}(j  =  0)
\mvdash{}  t  \mmember{}  Base  List


By

---

Latex:
xxx(HasValueD  (-2)  THEN  HVimplies2  (-3)  [1]  )xxx

---

Home Index