1. x : 
2. x':. x = rep_num(x')
3. m : 
4. 0<m
5. is_num_rep(rep_num(m-1))
  is_num_rep(rep_num(m))

1

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

4 steps

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