(19steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
find
intlist
great
bound
1
1
1.
x
:
List
{
y
:
|
i
:
||
x
||.
x
[
i
]<
y
}
By:
ListInd Hyp:1
Generated subgoals:
1
{
y
:
|
i
:
||nil||. nil[
i
]<
y
}
2
steps
2
2.
u
:
3.
v
:
List
4. {
y
:
|
i
:
||
v
||.
v
[
i
]<
y
}
{
y
:
|
i
:
||
u
.
v
||. (
u
.
v
)[
i
]<
y
}
14
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(19steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
List
{y:| 
i:
||x||. x[i]<y } List
{y:| i:||x||. x[i]<y } {y:| i:||nil||. nil[i]<y }
List
| i:||v||. v[i]<y }
{y:| i:||u.v||. (u.v)[i]<y }
