(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 3 1 1
1. x : 
2. P:(). P(zero_rep) & (n:. P(n)  P(suc_rep(n)))  P(x)
  x':. zero_rep = rep_num(x')  
By: ((DTerm 0 0) THEN (Unab [`hrep_num`])) THEN Simp THEN StrongAuto
THEN
Try (Complete (Unfold `hnum` 0))

Generated subgoals:

None

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

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