(248steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
world-event-system
3
1
1
1
1
2
1
1
1.
the_w
: World
2. FairFifo
3.
e
,
e'
:E. loc(
e
) = loc(
e'
)
e
<c
e'
e
=
e'
e'
<c
e
4.
e
:E. first(
e
)
(
e'
:E. loc(
e'
) = loc(
e
)
e'
<c
e
)
5.
t
:
6. 0<
t
7.
i
:Id.
7.
first(<
i
,
t
-1>)
7.
7.
loc(pred(<
i
,
t
-1>)) =
i
& time(pred(<
i
,
t
-1>))<
t
-1
7.
& (
e'
:E.
7. & (
(loc(pred(<
i
,
t
-1>)) = loc(
e'
) & time(pred(<
i
,
t
-1>))<time(
e'
)
7. & (
(
& loc(
e'
) =
i
7. & (
(
& time(
e'
)<
t
-1))
8.
t
= 0
9.
i
: Id
10. isnull(a(
i
;
t
-1))
11. first(<
i
,
t
-1>)
12.
first(<
i
,
t
-1>)
13. loc(pred(<
i
,
t
-1>)) =
i
& time(pred(<
i
,
t
-1>))<
t
-1
14.
e'
:E.
14.
(loc(pred(<
i
,
t
-1>)) = loc(
e'
) & time(pred(<
i
,
t
-1>))<time(
e'
)
14.
(
& loc(
e'
) =
i
14.
(
& time(
e'
)<
t
-1)
loc(pred(<
i
,
t
-1>)) =
i
Id & time(pred(<
i
,
t
-1>))<
t
By:
Analyze 0
Generated subgoals:
1
loc(pred(<
i
,
t
-1>)) =
i
Id
Auto
2
time(pred(<
i
,
t
-1>))<
t
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(248steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc