(13steps total)
PrintForm
Definitions
Lemmas
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
before-upto
2
1
2
1
2
1.
n
:
2.
x
:
n
3.
y
:
n
4.
x
<
y
5.
j
:
2
6.
j
= 0
7.
j
= 1
y
= upto(
n
)[
y
]
By:
Inst
Thm*
m
:
,
n
:
m
. upto(
m
)[
n
] =
n
[
n
;
y
]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
mb
event
system
1
Sections
EventSystems
Doc
j = 0
y = upto(n)[y]
m:
