1. m : 
2. a,r:.
2. iso_pair(;;is_num_rep;rep_num;abs_num)  rep_num(a) = r  a = abs_num(r)
3. m+1>0
  suc_rep(ncompose(suc_rep;m+1-1;zero_rep)) = suc_rep(rep_num(m))  

1

ncompose(suc_rep;m+1-1;zero_rep) = rep_num(m)

4 steps

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