---

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

No Annotations
∀[l:Base]. l ∈ Base List supposing (||l||)↓
BY
{ (Auto
   THEN All(RepUR ``length list_ind``)
   THEN Compactness (-1)
   THEN Unhide
   THEN Auto
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN RepeatFor 3 ((At ⌜Type⌝ (D 0)⋅ THENA Auto))
   THEN Try (Complete ((InstLemma `bottom_diverge` [] THEN Auto)))
   THEN (RWO "fun_exp_unroll" (-1) THENA Auto)
   THEN SplitOnHypITE (-1)
   THEN Auto
   THEN RepUR ``compose`` (-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. (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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[l:Base].  l  \mmember{}  Base  List  supposing  (||l||)\mdownarrow{}


By

---

Latex:
(Auto
  THEN  All(RepUR  ``length  list\_ind``)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  Auto
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  RepeatFor  3  ((At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))
  THEN  Try  (Complete  ((InstLemma  `bottom\_diverge`  []  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  (-1)
  THEN  Auto
  THEN  RepUR  ``compose``  (-2))

---

Home Index