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

Generated subgoal:

1 4. x' : 
5. n = rep_num(x')  
  suc_rep(n) = ncompose(suc_rep;x'+1;zero_rep)  
3 steps

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

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