(10steps total)
PrintForm
Definitions
Lemmas
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exponentiation
wf
nat
plus
1
1
1.
n
:
2.
k
:
3.
k1
:
.
k1
<
k
(
n
^
k1
)
(
n
^
k
)
By:
Compute
n
^
k
*
if
k
=
0
1 else
n
(
n
^(
k
-1)) fi THEN SplitOnConclITE
Generated subgoal:
1
4.
k
= 0
n
(
n
^(
k
-1))
7
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
HanoiTowers
Sections
NuprlLIB
Doc
k1:. k1<k 
(n^k1) 
(n^k)
k1:. k1<k (n^k1)
(n^k) if k=
0
1 else n
(n^(k-1)) fi THEN SplitOnConclITE
k = 0
n(n^(k-1)) 
