PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-join-list
wf
L
:MsgA List. (
A
,
B
L
.
A
||+
B
)
(
L
)
MsgA
By:
Inst
Thm*
L
:MsgA List.
Thm*
(
A
,
B
L
.
A
||+
B
)
(
L
)
MsgA & (
M
:MsgA. (
B
L
.
M
||+
B
)
M
||+
(
L
))
[]
THEN
RepeatFor 2 ParallelLast
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc
L:MsgA List. (A,B
L.A ||+ B) 
(L) MsgA L:MsgA List. (A,BL.A ||+ B) (L) MsgAL:MsgA List.
A,BL.A ||+ B) (L) MsgA & (M:MsgA. (BL.M ||+ B) M ||+ (L))
