1. m : 
2. 0<m
3. n:(m-1). upto(m-1)[n] = n
4. n : m
5. m = 0
6. n<m-1
  (upto(m-1) @ [(m-1)])[n] = n

By:	RWO Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] 0 THEN Try (RWO Thm* n:. ||upto(n)|| ~ n 0)

1

[(m-1)][(n-(m-1))] = n

1 step

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