(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
1
1
1.
n
:
2.
n1
:
.
n1
<
n
(
f
:(
).
f
(
n1
)
mu(
f
)
)
3.
f
:
4.
f
(
n
)
mu(
f
)
By:
Compute mu(
f
) *
if
f
(0)
0 else 1+mu(
x
.
f
(1+
x
)) fi
Generated subgoal:
1
if
f
(0)
0 else 1+mu(
x
.
f
(1+
x
)) fi
8
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
n1:
(
). f(n1) 
mu(f) 
0 else 1+mu(
x.f(1+x)) fi
