---

Step * 2 1 of Lemma length-wf-has-value


1. l : Base
2. (||l||)↓
3. ||l|| ≤ 0 + ||l||
4. (0 + ||l||)↓
⊢ ||l|| ∈ ℤ
BY
{ (HasValueD (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  Base
2.  (||l||)\mdownarrow{}
3.  ||l||  \mleq{}  0  +  ||l||
4.  (0  +  ||l||)\mdownarrow{}
\mvdash{}  ||l||  \mmember{}  \mBbbZ{}


By

---

Latex:
(HasValueD  (-1)  THEN  Auto)

---

Home Index