(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
1.
n
:
2.
x
:
n
3.
y
:
n
4.
x
<
y
j
:
2. [
x
;
y
][
j
] = upto(
n
)[if
j
=
0
x
else
y
fi]
By:
Auto THEN IntSegCases -1 THEN Reduce 0
Generated subgoals:
1
5.
j
:
2
6.
j
= 0
x
= upto(
n
)[
x
]
1
step
2
5.
j
:
2
6.
j
= 0
7.
j
= 1
y
= upto(
n
)[
y
]
1
step
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
x else y fi]
j = 0
