(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. x' : 
2. x'' : 
3. rep_num(x') = rep_num(x'')
4. n : 
5. 0<n
6. rep_num(0) = rep_num(n)
  0 = n  
By: Unab [`hrep_num`] THEN Simp THEN StrongAuto

Generated subgoal:

1 3. ncompose(suc_rep;x';zero_rep) = ncompose(suc_rep;x'';zero_rep)  
4. n : 
5. 0<n
6. zero_rep = suc_rep(ncompose(suc_rep;n-1;zero_rep))  
  0 = n  
11 steps

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

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