Nuprl - mb_event_system_7 LEMMAs for s_DASH_sframe_DASH

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
5	Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg) Dsys Thm* & (D:Dsys. Thm* & (@i: only L sends on (l with tg) D Thm* & ( Thm* & (D Thm* & (realizes es.e:E. Thm* & (realizes es.loc(e) = i Id null(sends(l,tg,e)) (kind(e) L))	[s-sframe-rule]
cites the following:
4	Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg) Thm* realizes es.e:E. loc(e) = i Id null(sends(l,tg,e)) (kind(e) L)	[sframe-rule]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html