---

Step * of Lemma MMTree-rank_wf

∀T:Type. ∀t:MMTree(T).  (MMTree-rank(t) ∈ ℕ)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN SimpleDatatypeInduction (-1)⋅ THEN RecUnfold `MMTree-rank` 0 THEN Reduce 0) }

1
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 ∈ ℕ

2
1. T : Type@i'
2. sz : ℕ
3. t1 : MMTree(T) List List
4. 0 < sz
5. ∀i:ℕ||t1||. ∀i1:ℕ||t1[i]||.  (MMTree_size(t1[i][i1]) ≤ (sz - 1))
6. ∀t:MMTree(T). MMTree-rank(t) ∈ ℕ supposing MMTree_size(t) ≤ (sz - 1)
⊢ imax-list([0 / map(λl.imax-list([0 / map(λs.MMTree-rank(s);l)]);t1)]) ∈ ℕ

---

Latex:


\mforall{}T:Type.  \mforall{}t:MMTree(T).    (MMTree-rank(t)  \mmember{}  \mBbbN{})


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  SimpleDatatypeInduction  (-1)\mcdot{}
  THEN  RecUnfold  `MMTree-rank`  0
  THEN  Reduce  0)

---

Home Index