1. n : 
2. x : n
3. y : n
4. f : 2||upto(n)||
5. increasing(f;2)
6. j:2. [x; y][j] = upto(n)[(f(j))]
7. x = upto(n)[(f(0))]
8. y = upto(n)[(f(1))]
  x<y

By:	RWO Thm* n:. ||upto(n)|| ~ n 4

1

4. f : 2n 5. increasing(f;2) 6. j:2. [x; y][j] = upto(n)[(f(j))] 7. x = upto(n)[(f(0))] 8. y = upto(n)[(f(1))]   x<y

2 steps

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