1. n : 
2. m : 
3. f : nm
4. Inj(n; m; f)
5. p : m( List)
6. sum(||p(j)|| | j < m) = n
7. j:m, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]
8. j:m, x:||p(j)||. (p(j))[x]<n & f((p(j))[x]) = j
9. j : m
  ||p(j)||1

1

10. x:||p(j)||. (p(j))[x]<n & f((p(j))[x]) = j 11. x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y] 12. ||p(j)||1   ||p(j)||1

6 steps

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