Nuprl - mb_event_system_7 LEMMAs for s_DASH_frame_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, x:Id, T:Type. Thm* @i: only members of L affect x :T Dsys Thm* & (D:Dsys. Thm* & (@i: only members of L affect x :T D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (((x after e) = (x when e) T (kind(e) L)) Thm* & (realizes es.& (& ((kind(e) L) (x after e) = (x when e) T)))	[s-frame-rule]
cites the following:
4	Thm* i:Id, L:Knd List, x:Id, T:Type. Thm* @i: only L affects x : T Thm* realizes es.(vartype(i;x) r T) Thm* realizes es.& (e:E. Thm* realizes es.& (loc(e) = i Id Thm* realizes es.& ( Thm* realizes es.& (((x after e) = (x when e) T (kind(e) L)) Thm* realizes es.& (& ((kind(e) L) (x after e) = (x when e) T))	[frame-rule]

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