---

Step * of Lemma length-wf-has-value

∀[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓
BY
{ (Auto THEN Assert ⌜||l|| ≤ 0 + ||l||⌝⋅) }

1
.....assertion..... 
1. l : Base
2. (||l||)↓
⊢ ||l|| ≤ 0 + ||l||

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

---

Latex:

---

Latex:
\mforall{}[l:Base].  ||l||  \mmember{}  \mBbbZ{}  supposing  (||l||)\mdownarrow{}


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}||l||  \mleq{}  0  +  ||l||\mkleeneclose{}\mcdot{})

---

Home Index