(15steps total)
Remark
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
kleene
minimize
wf
2
1.
n
:
,
f
:(
).
f
(
n
)
mu(
f
)
mu
{
f
:(
)|
x
:
.
f
(
x
) }
By:
With (Void
Void) (New:
f
FunExtensionality)
Generated subgoals:
1
mu
Void
Void
1
step
2
2.
f
: {
f
:(
)|
x
:
.
f
(
x
) }
mu(
f
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(15steps total)
Remark
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
n:
, f:(
). f(n) 
mu(f) 
mu {f:()| 
x:. f(x) }n:, f:(). f(n) mu(f)
mu {f:()| x:. f(x) }Void) (New:f FunExtensionality) mu VoidVoid
)| x:. f(x) }
mu(f) 
