(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. x : 
2. P:(). P(zero_rep) & (n:P(n P(suc_rep(n)))  P(x)
  x':x = rep_num(x' 


By: InstHyp [x:(x':x = rep_num(x'))] 2 THEN Simp THEN StrongAuto
THEN
Try (Complete (Unfold `hnum` 0))


Generated subgoals:

1   x':. zero_rep = rep_num(x' 
1 step
2 3. n : 
4. x':n = rep_num(x' 
  x':. suc_rep(n) = rep_num(x' 

4 steps

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

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