HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
n
,
k
:
. (
n
^
k
)
[exponentiation_wf_nat]
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
HanoiTowers
Sections
NuprlLIB
Doc
n,k:
. (n^k) 
i,j:. i
j n,k:. (n^k) i,j:. ij