mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
i
,
j
:
.
i
j
upto(
i
)
upto(
j
)
[upto_iseg]
cites the following:
1
Thm*
m
:
,
n
:
(
m
+1). upto(
m
) ~ (upto(
n
) @ map(
x
.
x
+
n
;upto(
m
-
n
)))
[upto_decomp]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
1
Sections
EventSystems
Doc
i,j:
. i
j 
upto(i) upto(j)m:, n:(m+1). upto(m) ~ (upto(n) @ map(
x.x+n;upto(m-n)))i,j:. ij upto(i) upto(j)m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))