---

Step * 2 of Lemma list-if-has-value-list_ind


1. b : Base@i
2. f : Base@i
3. ∀x:Base. strict(λu.f[x;u])
4. j : ℤ
5. 0 < j
6. ∀l:Base
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let a,b = v 
                                        in f[a;list_ind b] otherwise if v = Ax then b otherwise ⊥^j - 1 
       ⊥ 
       l)↓
     ⇒ (l ∈ Base List))
7. l : Base@i
8. (if l = Ax then b otherwise ⊥)↓@i
9. (l)↓
10. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
⊢ l ∈ Base List
BY
{ (HVimplies2 (-3) [1]
   THEN BotDiv
   THEN RW UnrollLoopsC 0
   THEN Reduce 0
   THEN Auto
   THEN Fold `it` 0
   THEN Fold `nil` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  Base@i
2.  f  :  Base@i
3.  \mforall{}x:Base.  strict(\mlambda{}u.f[x;u])
4.  j  :  \mBbbZ{}
5.  0  <  j
6.  \mforall{}l:Base
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  a,b  =  v 
                                                                              in  f[a;list$_{ind}$  b]  otherwise  if  v  =  A\000Cx  then  b  otherwise  \mbot{}\^{}j  -  1 
              \mbot{} 
              l)\mdownarrow{}
          {}\mRightarrow{}  (l  \mmember{}  Base  List))
7.  l  :  Base@i
8.  (if  l  =  Ax  then  b  otherwise  \mbot{})\mdownarrow{}@i
9.  (l)\mdownarrow{}
10.  \mforall{}a,b:Top.    (if  l  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  l  \mmember{}  Base  List


By

---

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

---

Home Index