1. m : 
2. 0<m
3. n:(m-1+1). upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))
4. n : (m+1)
5. n = m
6. m = 0
7. upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))
  ((upto(n) @ map(x.x+n;upto(m-1-n))) @ [(m-1)]) ~ (upto(n)
  @ map(x.x+n;upto(m-n)))

By:	RWO Thm* as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) 0 THEN Analyze THEN Try Trivial

1

(map(x.x+n;upto(m-1-n)) @ [(m-1)]) ~ map(x.x+n;upto(m-n))

5 steps

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