1. k : 
2. 0<k
3. P:((k-1)). 
3. ((i:(k-1). P(i))  0<search(k-1;P))
3. & (0<search(k-1;P)
3. & (
3. & (P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)))
4. P : k
5. ((i:(k-1). P(i))  0<search(k-1;P))
5. & (0<search(k-1;P)
5. & (
5. & (P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)))
6. (i:(k-1). P(i))
7. 0<search(k-1;P)
8. P(k-1)
  ((i:k. P(i))  0<k) & (0<k  P(k-1) & (j:k. j<k-1  P(j)))

1	5. (i:(k-1). P(i))  0<search(k-1;P) 6. (i:(k-1). P(i))  (0<search(k-1;P)) 7. 0<search(k-1;P) 7.  7. P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)) 8. (i:(k-1). P(i)) 9. 0<search(k-1;P) 10. P(k-1) 11. 0<k   i:k. P(i)	1 step
2	5. (i:(k-1). P(i))  0<search(k-1;P) 6. (i:(k-1). P(i))  (0<search(k-1;P)) 7. 0<search(k-1;P) 7.  7. P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)) 8. (i:(k-1). P(i)) 9. 0<search(k-1;P) 10. P(k-1) 11. 0<k 12. j : k 13. j<k-1   P(j)	1 step

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