---

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

∀l:Base. ((||l||)↓ ⇒ (||l|| ∈ ℕ))
BY
{ ((UnivCD THENA Auto)
   THEN All(RepUR ``length list_ind``)
   THEN Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl (-3)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN HasValueD (-1)
   THEN HVimplies2 (-2) [1]) }

1
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)> ∈ ℕ

2
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. (if l = Ax then 0 otherwise ⊥)↓
6. (l)↓
7. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
⊢ 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 ∈ ℕ

---

Latex:

---

Latex:
\mforall{}l:Base.  ((||l||)\mdownarrow{}  {}\mRightarrow{}  (||l||  \mmember{}  \mBbbN{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All(RepUR  ``length  list\_ind``)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  (-3)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)
  THEN  HVimplies2  (-2)  [1])

---

Home Index