1. x : 
2. P:(). P(zero_rep) & (n:. P(n)  P(suc_rep(n)))  P(x)
3. n : 
4. x' : 
5. n = rep_num(x')
  suc_rep(n) = ncompose(suc_rep;x'+1;zero_rep)  

1

6. x'+1>0   suc_rep(n) = suc_rep(ncompose(suc_rep;x'+1-1;zero_rep))

2 steps

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