---

Step * 2 of Lemma MMTree-rank_wf


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)]) ∈ ℕ
BY
{ ((GenConcl ⌈t1 = L ∈ ({L:MMTree(T) List| (L ∈ t1)}  List)⌉⋅ THENA Auto)
   THEN BLemma `imax-list-is-nat`
   THEN RepeatFor 2 (MemCD)
   THEN Try (CompleteAuto)
   THEN MemCD
   THEN Reduce 0
   THEN Try (CompleteAuto)
   THEN MemCD
   THEN Try (CompleteAuto)) }

1
.....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

---

Latex:



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)
\mvdash{}  imax-list([0  /  map(\mlambda{}l.imax-list([0  /  map(\mlambda{}s.MMTree-rank(s);l)]);t1)])  \mmember{}  \mBbbN{}


By

((GenConcl  \mkleeneopen{}t1  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  BLemma  `imax-list-is-nat`
  THEN  RepeatFor  2  (MemCD)
  THEN  Try  (CompleteAuto)
  THEN  MemCD
  THEN  Reduce  0
  THEN  Try  (CompleteAuto)
  THEN  MemCD
  THEN  Try  (CompleteAuto))

---

Home Index