mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* n,k:c:(nk).
Thm* p:(k( List)). 
Thm* sum(||p(j)|| | j < k) = n
Thm* & (j:kx,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
Thm* & (j:kx:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)
[finite-partition]

In prior sections: list 1 mb basic

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb nat Sections MarkB generic Doc