(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
2
1
2
1
1.
List
2.
u
:
3.
v
:
List
4.
w
:
5.
i
:
||
v
||.
v
[
i
]<
w
6.
u
<
w
7.
i
:
||
u
.
v
||
(
u
.
v
)[
i
]<
u
+2
By:
SideProof
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(19steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc