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:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]) Thm* & (j:k, x:||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