(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 4 1
1. x : 
2. x':. x = rep_num(x')
3. m : 
  is_num_rep(rep_num(m))
By: NInd -1 THEN Simp THEN StrongAuto

Generated subgoals:

1   is_num_rep(rep_num(0))
1 step
2 3. m : 
4. 0<m
5. is_num_rep(rep_num(m-1))
  is_num_rep(rep_num(m))
5 steps

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

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