(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.
n
:
2.
x
:
n
3.
y
:
n
4.
x
<
y
j
:
2. [
x
;
y
][
j
] = upto(
n
)[((
i
.if
i
=
0
x
else
y
fi)(
j
))]
By:
Reduce 0
Generated subgoal:
1
j
:
2. [
x
;
y
][
j
] = upto(
n
)[if
j
=
0
x
else
y
fi]
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:
i.if i=
0
x else y fi)(j))]
