Nuprl - mb_event_system_7 LEMMAs for better_DASH_sframe_DASH

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

Rank	Theorem	Name
6	Thm* L:Knd List, l:IdLnk, tg:Id. Thm* @source(l): only L sends on (l with tg) Dsys Thm* & (D:Dsys. Thm* & (@source(l): only L sends on (l with tg) D Thm* & ( Thm* & (D Thm* & (realizes es.e:E. Thm* & (realizes es.loc(e) = destination(l) Id Thm* & (realizes es. Thm* & (realizes es.kind(e) = rcv(l; tg) Knd (kind(sender(e)) L))	[better-sframe-rule]
cites the following:
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]
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]
0	Thm* the_es:ES, e:E. isrcv(e) index(e) \|\|sends(lnk(e);sender(e))\|\|	[es-index_wf]

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