mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
n
,
i
:
.
i
<
n
(
i
upto(
n
))
[member_upto2]
cites the following:
2
Thm*
m
:
,
n
:
m
. upto(
m
)[
n
] =
n
[select_upto]
1
Thm*
n
:
. ||upto(
n
)|| ~
n
[length_upto]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
1
Sections
EventSystems
Doc
n,i:
. i<n 
(i 
upto(n))m:, n:m. upto(m)[n] = nn:. ||upto(n)|| ~ nn,i:. i<n (i upto(n))m:, n:m. upto(m)[n] = nn:. ||upto(n)|| ~ n