(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
n
:
,
f
:(
).
f
(
n
)
mu(
f
)
By:
CompNatInd Concl THEN UnivCD
Generated subgoal:
1
1.
n
:
2.
n1
:
.
n1
<
n
(
f
:(
).
f
(
n1
)
mu(
f
)
)
3.
f
:
4.
f
(
n
)
mu(
f
)
9
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) 
n:, f:(). f(n) mu(f)
n1:. n1<n (f:(). f(n1) mu(f) )
mu(f) 
