k:, f:(kk). increasing(f;k)  (i:k. f(i) = i)

1

1. k :  2. 0<k 3. f:((k-1)(k-1)). increasing(f;k-1)  (i:(k-1). f(i) = i) 4. f : kk 5. increasing(f;k) 6. i : k   f(i) = i

16 steps

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