Nuprl - Proof: before-upto 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: before-upto 1 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))]
9. upto(n)[(f(0))] = f(0)
10. upto(n)[(f(1))] = f(1)

x<y

By:	Unfold `increasing` 5 THEN InstHyp [0] 5

Generated subgoals:

None

About:

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