---

Step * of Lemma MTree-rank_wf

∀T:Type. ∀tr:MultiTree(T).  (MTree-rank(tr) ∈ ℕ)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN SimpleDatatypeInduction 2 THEN RecUnfold `MTree-rank` 0 THEN Reduce 0) }

1
1. T : Type@i'
2. labels : {L:Atom List| 0 < ||L||} 
3. t2 : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)
4. ∀a:ℕ||labels||. (MTree-rank(t2 labels[a]) ∈ ℕ)
⊢ imax-list(map(λa.MTree-rank(t2 a);labels)) + 1 ∈ ℕ

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

---

Latex:


\mforall{}T:Type.  \mforall{}tr:MultiTree(T).    (MTree-rank(tr)  \mmember{}  \mBbbN{})


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  SimpleDatatypeInduction  2
  THEN  RecUnfold  `MTree-rank`  0
  THEN  Reduce  0)

---

Home Index