Nuprl Basics - Proof: kleene minimize is fp

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: kleene minimize is fp

f:{f:(

. f(x) }. f(mu(f))

By:	n:, f:{f:()\| x:. f(x) }. mu(f) = n f(mu(f)) Asserted

Generated subgoals:

1   n:, f:{f:()| x:. f(x) }. mu(f) = n  f(mu(f))
5 steps

2 1. n:, f:{f:()| x:. f(x) }. mu(f) = n  f(mu(f))
  f:{f:()| x:. f(x) }. f(mu(f))
1 step

About:

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

1	n:, f:{f:()\| x:. f(x) }. mu(f) = n f(mu(f))	5 steps
2	1. n:, f:{f:()\| x:. f(x) }. mu(f) = n f(mu(f)) f:{f:()\| x:. f(x) }. f(mu(f))	1 step