(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 2 1
1. n : 
2. k : 
3. k1:. k1<k  (n^k1)  
4. k = 0
5. n = 0
  x:. nx  
By: Auto

Generated subgoal:

1 6. x : 
  nx  
2 steps

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

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