(3steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
factbody
polytyping
(
f
,
x
. if
x
=
0
1 else
x
f
(
x
-1) fi)
(
k
:
. (
k
)
(
k
+1)
)
By:
3 Times Analyze
Generated subgoal:
1
1.
k
:
2.
f
:
k
3.
x
:
(
k
+1)
if
x
=
0
1 else
x
f
(
x
-1) fi
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
(
f,x. if x=
0
1 else x
f(x-1) fi) 
(
k:
. (k
)(k+1)) (f,x. if x=0 1 else xf(x-1) fi) (k:. (k)(k+1))
k
(k+1)
if x=0 1 else xf(x-1) fi 
