---

Step * 2 1 of Lemma MMTree-rank_wf

.....subterm..... T:t
2: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
⊢ map(λs.MMTree-rank(s);l) ∈ ℤ List
BY
{ ((GenConcl ⌈l = X ∈ ({t:MMTree(T)| (t ∈ l)}  List)⌉⋅ THENA Auto) THEN RepeatFor 2 (MemCD) THEN Try (CompleteAuto)) }

1
.....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) ∈ ℤ

---

Latex:


.....subterm.....  T:t
2: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
\mvdash{}  map(\mlambda{}s.MMTree-rank(s);l)  \mmember{}  \mBbbZ{}  List


By

((GenConcl  \mkleeneopen{}l  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (MemCD)  THEN  Try  (CompleteAuto))

---

Home Index