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
  sum(if c(n-1)=j ||[(n-1) / (p(j))]|| else ||p(j)|| fi | j < k) = n

By:	Reduce 0 THEN RWO Thm* k:, f,g:(k), p:(k). Thm* sum(if p(i) f(i)+g(i) else f(i) fi | i < k) Thm* = Thm* sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) 0 THEN HypSubst' -3 0

1

n-1+sum(if c(n-1)=j 1 else 0 fi | j < k) = n

5 steps

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