NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
(
f
,
x
. if
x
=
0
1 else
x
f
(
x
-1) fi)
(
k
:
. (
k
)
(
k
+1)
)
[sfa_doc_factbody_polytyping]
cites the following:
2
Thm*
i
,
j
:
.
i
j
[multiply_nat_wf]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NuprlPrimitives
Sections
NuprlLIB
Doc
f,x. if x=
0
1 else x
f(x-1) fi) 
(
k:
. (k
)(k+1))
i,j:. ij f,x. if x=0 1 else xf(x-1) fi) (k:. (k)(k+1))i,j:. ij