(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 2 1 1
1. x : 
2. x':. x = ncompose(suc_rep;x';zero_rep)
3. m : 
4. 0<m
5. P:(). 
5. P(zero_rep) & (n:. P(n)  P(suc_rep(n)))
5. 
5. P(ncompose(suc_rep;m-1;zero_rep))
6. P : 
7. P(zero_rep)
8. n:. P(n)  P(suc_rep(n))
  P(suc_rep(ncompose(suc_rep;m-1;zero_rep)))
By: InstHyp [P] 5 THEN Simp THEN StrongAuto

Generated subgoals:

1 9. n : 
10. P(n)
  P(suc_rep(n))
1 step
2 9. P(ncompose(suc_rep;m-1;zero_rep))
  P(suc_rep(ncompose(suc_rep;m-1;zero_rep)))
1 step

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

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