---

Step * of Lemma length_nil

||[]|| = 0 ∈ ℤ
BY
{ (AbReduce 0 THEN Auto{1,3}-1) }

---

Latex:

---

Latex:
||[]||  =  0


By

---

Latex:
(AbReduce  0  THEN  Auto\{1,3\}-1)

---

Home Index