Nuprl Basics - Proof: sfa doc find small greater bound 1 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc find small greater bound 1 2 1 1 1

1. k :

k List
3. u :

k
4. v :

k List
5. y :

(k+1)
6. y greater-bounds v
7. u<y

y greater-bounds u.v

By:	Def of <int> greater-bounds <int list> THEN Decide: 0<i

Generated subgoals:

1 8. i : ||u.v||
9. 0<i
(u.v)[i]<y
3 steps

2 8. i : ||u.v||
9. 0<i
(u.v)[i]<y
1 step

About:

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

1	8. i : \|\|u.v\|\| 9. 0<i (u.v)[i]<y	3 steps
2	8. i : \|\|u.v\|\| 9. 0<i (u.v)[i]<y	1 step