Nuprl - Proof: finite-partition 2 2 1 1

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

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,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]
11. c(n-1) = j

x@0,y:||[(n-1) / (p(j))]||. x@0 < y [(n-1) / (p(j))][x@0] > [(n-1) / (p(j))][y]

By: Reduce 0 THEN Analyze 0 THEN Analyze 0 THEN CaseNat 0 `x@0' THEN Reduce 0 THEN RWW Thm* a:T, as:T List, i:. 0 < i i||as|| [a / as][i] = as[(i-1)] 0

Generated subgoals:

1 12. x@0: (||p(j)||+1)
13. y: (||p(j)||+1)
14. x@0 = 0
15. 0 < y
n-1 > (p(j))[(y-1)] 1 step

2 12. x@0: (||p(j)||+1)
13. y: (||p(j)||+1)
14. x@0 = 0
15. x@0 < y
(p(j))[(x@0-1)] > (p(j))[(y-1)] 1 step

About:

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

1	12. `x@0:` `(\|\|p(j)\|\|+1)` 13. `y:` `(\|\|p(j)\|\|+1)` 14. `x@0 = 0` 15. `0 < y` `n-1 > (p(j))[(y-1)]`	1 step

2	12. `x@0:` `(\|\|p(j)\|\|+1)` 13. `y:` `(\|\|p(j)\|\|+1)` 14. `x@0 = 0` 15. `x@0 < y` `(p(j))[(x@0-1)] > (p(j))[(y-1)]`	1 step