(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
1
1.
n
:
2.
x
:
n
3.
y
:
n
4.
f
:
2
||upto(
n
)||
5. increasing(
f
;2)
6.
j
:
2. [
x
;
y
][
j
] = upto(
n
)[(
f
(
j
))]
x
<
y
By:
InstHyp [0] -1 THEN InstHyp [1] -2 THEN All Reduce
Generated subgoal:
1
7.
x
= upto(
n
)[(
f
(0))]
8.
y
= upto(
n
)[(
f
(1))]
x
<
y
3
steps
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:
x<y
