(6steps 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 1 1 1
1. n : 
2. k : 
3. k1:. k1<k  (n^k1)  
4. k = 0
  n(n^(k-1))  
By: BackThru: Thm*  i,j:. ij  

Generated subgoals:

1   n  
Trivial
2   (n^(k-1))  
1 step

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

(6steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc