n,k:, c:(nk).
  p:(k( List)). 
  sum(||p(j)|| | j < k) = n
  & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
  & (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)

1	k:, c:(0k).   p:(k( List)).    sum(||p(j)|| | j < k) = 0   & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])   & (j:k, x:||p(j)||. (p(j))[x]<0 & c((p(j))[x]) = j)	2 steps
2	1. n :  2. 0<n 3. k:, c:((n-1)k). 3. p:(k( List)).  3. sum(||p(j)|| | j < k) = n-1 3. & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]) 3. & (j:k, x:||p(j)||. (p(j))[x]<n-1 & c((p(j))[x]) = j)   k:, c:(nk).   p:(k( List)).    sum(||p(j)|| | j < k) = n   & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])   & (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)	23 steps

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