---

Step * 1 1 of Lemma C_TYPE-valueall-type


1. sz : ℕ
2. ∀sz:ℕsz. ∀v:C_TYPE().  (evalall(v))↓ supposing C_TYPE_size(v) ≤ sz
3. 0 ≤ sz
⊢ 0 ≤ 0
BY
{ Auto }

---

Latex:

---

Latex:

1.  sz  :  \mBbbN{}
2.  \mforall{}sz:\mBbbN{}sz.  \mforall{}v:C\_TYPE().    (evalall(v))\mdownarrow{}  supposing  C\_TYPE\_size(v)  \mleq{}  sz
3.  0  \mleq{}  sz
\mvdash{}  0  \mleq{}  0


By

---

Latex:
Auto

---

Home Index