Nuprl - Proof: upto decomp 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: upto decomp 2

1. m :

2. 0<m
3.

(m-1+1). upto(m-1) ~ (upto(n) @ map(

x.x+n;upto(m-1-n)))
4. n :

(m+1)

upto(m) ~ (upto(n) @ map(

x.x+n;upto(m-n)))

By:	Decide (n = m)

Generated subgoals:

1 5. n = m
upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
1 step

2 5. n = m
upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
9 steps

About:

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

1	5. n = m upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	1 step
2	5. n = m upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	9 steps