IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
kleene minimize is fp2 1. n:, f:{f:()| x:. f(x) }. mu(f) = nf(mu(f))
f:{f:()| x:. f(x) }. f(mu(f))
By:
Auto THEN BackThru: Hyp:1 Using:[mu(f)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
, f:{f:(
)| 
x:
f(mu(f))
