Nuprl - Proof: select upto 1

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

1. m :

2. 0<m
3.

(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)[i] = as[i] 0 THEN Try (RWO Thm* n:. \|\|upto(n)\|\| ~ n 0) THEN Try BackThruSomeHyp

Generated subgoals:

None

About:

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