(8steps total)
PrintForm
Definitions
mb
event
system
7
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
send-once
realizes
1
1
2
1
1.
T
: Type
2.
A
: Type
3.
a
: Id
4.
f
:
A
T
5.
tg
: Id
6.
l
: IdLnk
7.
x
: Id
8.
"done" =
x
9.
A
10.
T
11. (
loc
.
(send-once(
loc
;
T
;
A
;
a
;
f
;
tg
;
l
;
x
)))
Dsys
12.
D'
: Dsys
13.
loc
.
(send-once(
loc
;
T
;
A
;
a
;
f
;
tg
;
l
;
x
))
D'
14.
w
: World
15.
p
: FairFifo
16. PossibleWorld(
D'
;
w
)
17.
e
: E
18. loc(
e
) = source(
l
)
19. kind(
e
) = locl(
a
)
20.
e
:E.
20.
loc(
e
) = source(
l
)
20.
20.
(
e'
:E.
20. (
loc(
e'
) = source(
l
)
kind(
e
) = locl(
a
)
kind(
e'
) = locl(
a
)
e
=
e'
)
21. @source(
l
): ma-single-sends1(
A
; Unit;
T
;
x
; locl(
a
);
l
;
tg
; (
a
,
b
. [(
f
(
a
))])
21. @source(
l
): ma-single-sends1(
)
21.
Dsys
22. vartype(source(
l
);
x
)
r
A
23.
e
:E. loc(
e
) = source(
l
)
kind(
e
) = locl(
a
)
(valtype(
e
)
r Unit)
24.
e
:E. kind(
e
) = rcv(
l
;
tg
)
(valtype(
e
)
r
T
)
25.
e
:E.
25.
loc(
e
) = source(
l
)
25.
25.
kind(
e
) = locl(
a
)
25.
25.
(
e'
:E.
25. (
kind(
e'
) = rcv(
l
;
tg
)
25. (
& sender(
e'
) =
e
25. (&
& (
e''
:E. kind(
e''
) = rcv(
l
;
tg
)
sender(
e''
) =
e
e''
=
e'
)
25. (&
& val(
e'
) =
f
((
x
when
e
)))
26.
e'
: E
27. kind(
e'
) = rcv(
l
;
tg
)
28. sender(
e'
) =
e
29.
e''
:E. kind(
e''
) = rcv(
l
;
tg
)
sender(
e''
) =
e
e''
=
e'
30. val(
e'
) =
f
((
x
when
e
))
31.
e'@0
: E
32. kind(
e'@0
) = rcv(
l
;
tg
)
33. kind(sender(
e'@0
)) = locl(
a
)
sender(
e'@0
) =
e
E
By:
AllHyps (
h.BackThru h THEN Complete MaAuto)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
mb
event
system
7
Sections
EventSystems
Doc