---

Step * 2 of Lemma MTree-rank_wf


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

---

Latex:



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


By

Auto

---

Home Index