Nuprl Basics - Proof: sfa doc find small greater bound 1 2 1 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

1. k :

k List
3. u :

k
4. v :

k List
5. y :

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

||u.v||
9. 0<i

(u.v)[i]<y

By:	Rewrite by Thm* a:T, as:T List, i:. 0<i i\|\|as\|\| (a.as)[i] = as[(i-1)]

Generated subgoal:

1 v[(i-1)]<y
2 steps

About:

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