Def  n^k == if k=0 1 else n(n^(k-1)) fi  (recursive)

is mentioned by

Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q) Thm*  ( Thm*  ((2^n)z-a+1)	[hanoi_sol2_lb]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1)	[hanoi_general_exists_lemma2PROG_endpoint]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html