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)) }
4. p : k
5. i : k
6. p(i)
7. p(0)
8. (least i:. p(i+1))  {i:(k-1)| p(i+1) & (j:i. p(j+1)) }
  (least i:. p(i+1))+1  {i:k| p(i) & (j:i. p(j)) }

1

8. (least i:. p(i+1))  (k-1) 9. p((least i:. p(i+1))+1) 10. j:(least i:. p(i+1)). p(j+1)   (least i:. p(i+1))+1  {i:k| p(i) & (j:i. p(j)) }

4 steps

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