(26steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: finite-partition 2 2 2 1 2 1
1. n:
2. 0 < n
3. k:
4. c: nk
5. p: k( List)
6. sum(||p(j)|| | j < k) = n-1
7. j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]
8. j:k, x:||p(j)||. (p(j))[x] < n-1 & c((p(j))[x]) = j
9. j: k
10. x:||p(j)||. (p(j))[x] < n-1 & c((p(j))[x]) = j
11. c(n-1) = j
12. x@0: (||p(j)||+1)
13. x@0 = 0
14. (p(j))[(x@0-1)] < n-1
15. c((p(j))[(x@0-1)]) = j
[(n-1) / (p(j))][x@0] < n & c([(n-1) / (p(j))][x@0]) = j
By: Analyze 0
Generated subgoals:

1 [(n-1) / (p(j))][x@0] < n1 step
 
216. [(n-1) / (p(j))][x@0] < n
c([(n-1) / (p(j))][x@0]) = j		2 steps

About:
listconsintnatural_numberaddsubtractless_than
applyfunctionequalimpliesall

(26steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc