1. k : 
2. 0<k
3. p:{p:((k-1))| i:(k-1). p(i) }. 
3. (least i:. p(i))  {i:(k-1)| p(i) & (j:i. p(j)) }
  p:{p:(k)| i:k. p(i) }. 
  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }

By:	Compute least i:. p(i) * if p(0) 0 else (least i:. p(i+1))+1 fi THEN UnivCD THEN Analyze-1 THEN Analyze-1

1

4. p : k 5. i : k 6. p(i)   if p(0) 0 else (least i:. p(i+1))+1 fi  {i:k| p(i) & (j:i. p(j)) }

14 steps

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