---

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


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

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  (||snd(l)||  +  1)  =  0
3.  (||snd(l)||  +  1)\mdownarrow{}
4.  0  \mleq{}  0
5.  l  \msim{}  <fst(l),  snd(l)>
6.  ||snd(l)||  \mmember{}  \mBbbZ{}
7.  1  \mmember{}  \mBbbZ{}
8.  ||snd(l)||  \mmember{}  \mBbbN{}
\mvdash{}  <fst(l),  snd(l)>  =  []


By

---

Latex:
Auto'

---

Home Index