IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
kleene minimize is lb2 1. n:, f:{f:()| x:. f(x) }. mu(f) = n (i:. i<mu(f) f(i))
f:{f:()| x:. f(x) }, i:. i<mu(f) f(i)
By:
Auto THEN BackThru: Hyp:1 Using:[mu(f)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
, f:{f:(
)| 
x:
(
f(i))
