IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite-partition
2
2
1
1
2
1. n :
2. 0<n
3. k :
4. c :
n

k
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
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)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html