---

Step * 1 1 1 of Lemma length-zero-implies-nil


1. l : Base@i
2. ||<fst(l), snd(l)>|| = 0 ∈ ℤ
3. (rec-case(snd(l)) of [] => 0 | h::t => r.r + 1 + 1)↓
4. 0 ≤ 0
5. l ~ <fst(l), snd(l)>
⊢ <fst(l), snd(l)> = [] ∈ Base
BY
{ (Fold `length` (-3) THEN HasValueD (-3)) }

1
1. l : Base@i
2. ||<fst(l), snd(l)>|| = 0 ∈ ℤ
3. (||snd(l)|| + 1)↓
4. 0 ≤ 0
5. l ~ <fst(l), snd(l)>
6. ||snd(l)|| ∈ ℤ
7. 1 ∈ ℤ
⊢ <fst(l), snd(l)> = [] ∈ Base

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  ||<fst(l),  snd(l)>||  =  0
3.  (rec-case(snd(l))  of  []  =>  0  |  h::t  =>  r.r  +  1  +  1)\mdownarrow{}
4.  0  \mleq{}  0
5.  l  \msim{}  <fst(l),  snd(l)>
\mvdash{}  <fst(l),  snd(l)>  =  []


By

---

Latex:
(Fold  `length`  (-3)  THEN  HasValueD  (-3))

---

Home Index