1. n : 
2. n1:. 
2. n1<n  (f:{f:()| x:. f(x) }. mu(f) = n1  (i:. i<mu(f)  f(i)))
  f:{f:()| x:. f(x) }. 
  if f(0) 0 else 1+mu(x.f(1+x)) fi = n  
  
  (i:. i<if f(0) 0 else 1+mu(x.f(1+x)) fi  f(i))

1

3. f : {f:()| x:. f(x) }   if f(0) 0 else 1+mu(x.f(1+x)) fi = n        (i:. i<if f(0) 0 else 1+mu(x.f(1+x)) fi  f(i))

5 steps

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