(46steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 1 1 1 2 2 2 1 1
1. 
2. 
3. n : 
4. 0<n
5. x:. 0 = x+1
  False
By: Analyze 5

Generated subgoals:

None

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc