---

Step * 2 1 1 of Lemma MMTree-rank_wf

.....subterm..... T:t
1:n
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)
7. L : {L:MMTree(T) List| (L ∈ t1)}  List@i
8. t1 = L ∈ ({L:MMTree(T) List| (L ∈ t1)}  List)@i
9. l : {L:MMTree(T) List| (L ∈ t1)} @i
10. X : {t:MMTree(T)| (t ∈ l)}  List@i
11. l = X ∈ ({t:MMTree(T)| (t ∈ l)}  List)@i
12. s : {t:MMTree(T)| (t ∈ l)} @i
⊢ MMTree-rank(s) ∈ ℤ
BY
{ (DSetVars THEN D -5 THEN D -1 THEN BackThruSomeHyp THEN Auto) }

---

Latex:


.....subterm.....  T:t
1:n
1.  T  :  Type@i'
2.  sz  :  \mBbbN{}
3.  t1  :  MMTree(T)  List  List
4.  0  <  sz
5.  \mforall{}i:\mBbbN{}||t1||.  \mforall{}i1:\mBbbN{}||t1[i]||.    (MMTree\_size(t1[i][i1])  \mleq{}  (sz  -  1))
6.  \mforall{}t:MMTree(T).  MMTree-rank(t)  \mmember{}  \mBbbN{}  supposing  MMTree\_size(t)  \mleq{}  (sz  -  1)
7.  L  :  \{L:MMTree(T)  List|  (L  \mmember{}  t1)\}    List@i
8.  t1  =  L@i
9.  l  :  \{L:MMTree(T)  List|  (L  \mmember{}  t1)\}  @i
10.  X  :  \{t:MMTree(T)|  (t  \mmember{}  l)\}    List@i
11.  l  =  X@i
12.  s  :  \{t:MMTree(T)|  (t  \mmember{}  l)\}  @i
\mvdash{}  MMTree-rank(s)  \mmember{}  \mBbbZ{}


By

(DSetVars  THEN  D  -5  THEN  D  -1  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index