At: least characterized

  k:, p:{p:(k)| i:k. p(i) }.
  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }

1	p:{p:(0)| i:0. p(i) }.    (least i:. p(i))  {i:0| p(i) & (j:i. p(j)) }	1 step
2	1. k :  2. 0<k 3. p:{p:((k-1))| i:(k-1). p(i) }.  3. (least i:. p(i))  {i:(k-1)| p(i) & (j:i. p(j)) }   p:{p:(k)| i:k. p(i) }.    (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }	15 steps

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