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)

By:	Auto THEN InstConcl [j.nil] THEN Reduce 0 THEN Try (RWO Thm* n:, a:. sum(a | x < n) = an 0)

1

1. k :  2. 0k 3. p : k( List) 4. j : k 5. x : ||p(j)|| 6. (p(j))[x]<0   p(j)  0 List

1 step

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