(26steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-partition 2 2 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
  x@0:||[(n-1) / (p(j))]||. 
  [(n-1) / (p(j))][x@0]<n & c([(n-1) / (p(j))][x@0]) = j
By: Reduce 0 THEN Analyze 0 THEN CaseNat 0 `x@0' THEN Reduce 0

Generated subgoals:

1 12. x@0 : (||p(j)||+1)
13. x@0 = 0
  n-1<n & c(n-1) = j
Auto
2 12. x@0 : (||p(j)||+1)
13. x@0 = 0
  [(n-1) / (p(j))][x@0]<n & c([(n-1) / (p(j))][x@0]) = j
5 steps

About:
listconsintnatural_numbersubtractless_thanapplyfunctionequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(26steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc