1. m : 
2. n : 
3. P : 
4. n:. P(n+1)  P(n)
5. P(m)
6. P(n)
7. m>n
8. k : 
9. 0<k
10. 0n+k-1  P(n+k-1)  P(n)
11. 0n+k
12. P(n+k)
  0n+k-1

By:	Assert (0+0n+k-1) THEN StrongAuto

1

0+0n+k-1

Auto

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