Nuprl - Proof: upto decomp 2 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: upto decomp 2 2 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)
5.

n = m
6.

m = 0

(upto(m-1) @ [(m-1)]) ~ (upto(n) @ map(

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

By:	InstHyp [n] 3 THEN Subst (upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))) 0 THEN Try Trivial

Generated subgoal:

1 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)))
6 steps

About:

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