---

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


1. l : Base
2. (||l||)↓
3. ||l|| ≤ 0 + ||l||
⊢ ||l|| ∈ ℤ
BY
{ (FLemma `has-value-monotonic` [-1;-2] THEN Auto) }

1
1. l : Base
2. (||l||)↓
3. ||l|| ≤ 0 + ||l||
4. (0 + ||l||)↓
⊢ ||l|| ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
(FLemma  `has-value-monotonic`  [-1;-2]  THEN  Auto)

---

Home Index