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

List
2. u :

3. v :

List
4. w :

||v||. v[i]<w [not for witness]

{y:

||u.v||. (u.v)[i]<y }

By:	Decide: u<w

Generated subgoals:

1 6. u<w
{y:| i:||u.v||. (u.v)[i]<y }
6 steps

2 6. u<w
{y:| i:||u.v||. (u.v)[i]<y }
6 steps

About:

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

1	6. u<w {y:\| i:\|\|u.v\|\|. (u.v)[i]<y }	6 steps
2	6. u<w {y:\| i:\|\|u.v\|\|. (u.v)[i]<y }	6 steps