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:
not
locl
rcv
a
:Id,
l
:IdLnk,
tg
:Id. locl(
a
) = rcv(
l
;
tg
)
False
By:
Auto THEN Assert (rcv(
l
;
tg
) = locl(
a
))
THEN
FwdThru
Thm*
a
:Id,
l
:IdLnk,
tg
:Id. rcv(
l
;
tg
) = locl(
a
)
False [-1]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
event
system
1
Sections
EventSystems
Doc
a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg) 
False a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg) Falsea:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a) False [-1]
