---

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


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
BY
{ (Fold `cons` 2 THEN Reduce 2 THEN (InstLemma `length-nat-if-has-value` [⌜snd(l)⌝]⋅ THENA Auto)) }

1
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

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  ||<fst(l),  snd(l)>||  =  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{}
\mvdash{}  <fst(l),  snd(l)>  =  []


By

---

Latex:
(Fold  `cons`  2  THEN  Reduce  2  THEN  (InstLemma  `length-nat-if-has-value`  [\mkleeneopen{}snd(l)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index