1. n : 
2. n1:. n1<n  (f:{f:()| x:. f(x) }. mu(f) = n1  f(mu(f)))
3. f : {f:()| x:. f(x) }
4. mu(f) = n
5. f(0)
6. (x.f(1+x))  {f:()| x:. f(x) }
  mu(x.f(1+x))<n

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

1

4. if f(0) 0 else 1+mu(x.f(1+x)) fi = n   5. f(0) 6. (x.f(1+x))  {f:()| x:. f(x) }   mu(x.f(1+x))<n

1 step

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