Nuprl - mb_event_system_6 LEMMAs for s_DASH_effect_DASH

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

Rank	Theorem	Name
6	Thm* i,x:Id, a:Knd, T,A:Type, f:(ATA). Thm* @i: ma-single-effect0(x;A;a;T;f) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-effect0(x;A;a;T;f) D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r A) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = a Knd (valtype(e) r T)) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = a Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((x after e) = f((x when e),val(e)) A))	[s-effect-rule0]
cites the following:
5	Thm* i,x:Id, k:Knd, ds:a:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* @i: ma-single-effect(ds; da; k; x; f) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-effect(ds; da; k; x; f) D Thm* & ( Thm* & (D Thm* & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((x after e) = f((z.(z when e)),val(e)) ds(x)?Top))	[s-effect-rule]

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