Nuprl - Proof: before-upto 1 1 1

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

1. n :

2. x :

n
3. y :

n
4. f :

n
5. increasing(f;2)
6.

2. [x; y][j] = upto(n)[(f(j))]
7. x = upto(n)[(f(0))]
8. y = upto(n)[(f(1))]

x<y

By:	Inst Thm* m:, n:m. upto(m)[n] = n [n;f(0)] THEN Inst Thm* m:, n:m. upto(m)[n] = n [n;f(1)]

Generated subgoal:

1 9. upto(n)[(f(0))] = f(0)
10. upto(n)[(f(1))] = f(1)
x<y
1 step

About:

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