IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
upto decomp2221122 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)))
8. m-n = 0
[(m-1)] ~ map(x.x+n;[(m-n-1)])
By:
Reduce 0 THEN Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html