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) }. mu(f) = n  (i:. i<mu(f)  f(i))

By:	Compute mu(f) * if f(0) 0 else 1+mu(x.f(1+x)) fi

1

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))

6 steps

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