Nuprl Basics - Proof: sfa doc find intlist great bound 1 1 2 1 2 1 a 1

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

List
2. u :

3. v :

List
4. w :

||v||. v[i]<w
6.

u<w
7. i :

||u.v||
8. 0<i

(u.v)[i]<u+2

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)]<u+2
1 step

About:

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