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. i:k. P(i)
  ((i:k. P(i))  0<search(k;P))
  & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))

1	5. 0<search(k-1;P) 6. P(search(k-1;P)-1) 7. j:(k-1). j<search(k-1;P)-1  P(j) 8. i1 : (k-1) 9. P(i1) 10. i : k 11. P(i)   search(k;P) = search(k-1;P)	2 steps
2	5. 0<search(k-1;P) 6. P(search(k-1;P)-1) & (j:(k-1). j<search(k-1;P)-1  P(j)) 7. i1 : (k-1) 8. P(i1) 9. i : k 10. P(i)   ((i:k. P(i))  0<search(k-1;P))   & (0<search(k-1;P)   & (   & (P(search(k-1;P)-1) & (j:k. j<search(k-1;P)-1  P(j)))	2 steps

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