(7steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
kleene
minimize
is
fp
1
n
:
,
f
:{
f
:(
)|
x
:
.
f
(
x
) }. mu(
f
) =
n
f
(mu(
f
))
By:
CompNatInd Concl
Generated subgoal:
1
1.
n
:
2.
n1
:
.
n1
<
n
(
f
:{
f
:(
)|
x
:
.
f
(
x
) }. mu(
f
) =
n1
f
(mu(
f
)))
3.
f
: {
f
:(
)|
x
:
.
f
(
x
) }
4. mu(
f
) =
n
f
(mu(
f
))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
n:
, f:{f:(
)| 
x:. f(x) }. mu(f) = n 
f(mu(f)) n:, f:{f:()| x:. f(x) }. mu(f) = n f(mu(f))
n1:. n1<n (f:{f:()| x:. f(x) }. mu(f) = n1 f(mu(f)))
)| x:. f(x) }
f(mu(f))
