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)
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. 0<search(k-1;P)
9. P(k-1)
10. i : k
11. P(i)
  i<k-1

1

9. i : k 10. P(i) 11. i<k-1   P(k-1)

1 step

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