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
  (j:k, x,y:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.
  (x<y
  (
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>if c(n-1)=j
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>if [(n-1) / (p(j))]
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>else p(j) fi[y])
  & (j:k, x:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.
  & (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]<n
  & (& c(if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]) = j)

1	j:k, x,y:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.   x<y      if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>if c(n-1)=j [(n-1) / (p(j))]   if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>else p(j) fi[y]	4 steps
2	j:k, x:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.   if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]<n   & c(if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]) = j	9 steps

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