1. x : 
2. x':. x = ncompose(suc_rep;x';zero_rep)
3. m : 
4. 0<m
5. is_num_rep(ncompose(suc_rep;m-1;zero_rep))
  is_num_rep(suc_rep(ncompose(suc_rep;m-1;zero_rep)))

1

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)))

3 steps

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