Def mu(f) == if f(0) 0 else 1+mu(x.f(1+x)) fi  (recursive)

is mentioned by

Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(mu(f))	[kleene_minimize_is_fp]

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