---

Step * 1 of Lemma MMTree-rank_wf


1. T : Type@i'
2. sz : ℕ
3. ∀sz:ℕsz. ∀t:MMTree(T).  MMTree-rank(t) ∈ ℕ supposing MMTree_size(t) ≤ sz
4. t1 : T
5. 0 ≤ sz
⊢ 0 ∈ ℕ
BY
{ Auto }

---

Latex:



1.  T  :  Type@i'
2.  sz  :  \mBbbN{}
3.  \mforall{}sz:\mBbbN{}sz.  \mforall{}t:MMTree(T).    MMTree-rank(t)  \mmember{}  \mBbbN{}  supposing  MMTree\_size(t)  \mleq{}  sz
4.  t1  :  T
5.  0  \mleq{}  sz
\mvdash{}  0  \mmember{}  \mBbbN{}


By

Auto

---

Home Index