Nuprl - mb_event_system_7 LEMMAs for s_DASH_pre_DASH_init_DASH_rule1

mb event system 7 Sections EventSystems Doc

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

Rank	Theorem	Name
9	Thm* i,a,x:Id, A,T:Type, c:A, P:(ATProp). Thm* @i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v)) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v)) D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r A) Thm* & (realizes es.& (e:E. loc(e) = i Id first(e) (x when e) = c A) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(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) = locl(a) Knd P((x when e),val(e))) Thm* & (realizes es.& & ((v:T. P(c,v)) Thm* & (realizes es.& & ( Thm* & (realizes es.& & ((e:E. Thm* & (realizes es.& & ((loc(e) = i Id Thm* & (realizes es.& & ((& kind(e) = locl(a) Knd Thm* & (realizes es.& & ((& (v:T. P((x after e),v)))))	[s-pre-init-rule1]
cites the following:
5	Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp), Thm* init:x:Id fp-> ds(x)?Void. Thm* (x:Id. x dom(ds) x dom(init)) Thm* Thm* @i: (with ds: ds init: initaction a:T precondition a(v) is P) Dsys Thm* & (D:Dsys. Thm* & (@i: (with ds: ds Thm* & (@init: init Thm* & (action a:T Thm* & (aprecondition a(v) is Thm* & (aP) D Thm* & ( Thm* & (D Thm* & (realizes es.(v:T. P((x.init(x)?),v)) (e:E. loc(e) = i Id))	[s-pre-init-rule]
6	Thm* i,a,x:Id, A,T:Type, P:(ATProp). Thm* @i: ma-single-pre1(x;A;a;T;x,v.P(x,v)) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v)) 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) = locl(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) = locl(a) Knd P((x when e),val(e))) Thm* & (realizes es.& (& (e':E. Thm* & (realizes es.& (& ((e <loc e') e = e' E Thm* & (realizes es.& (& (& kind(e') = locl(a) Knd Thm* & (realizes es.& (& (& (v:T. P((x after e'),v)))))	[s-pre-rule1]
5	Thm* i:Id, T:Type, v:T, x:Id. Thm* @i: x : T initially x = v Dsys Thm* & (D:Dsys. Thm* & (@i: x : T initially x = v D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& (e:E. loc(e) = i Id first(e) (x when e) = v T))	[s-init-rule]
8	Thm* D1,D2,D3:Dsys. D1 D2 D2 D3 D1 D3	[d-sub_transitivity]
2	Thm* i:Id, A,B:MsgA. @i: A @i: B A B	[s-at-sub-s-at]
0	Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g f g	[fpf-sub_weakening]
0	Thm* B,eq,g:Top. g	[fpf-empty-sub]
1	Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v x : v	[fpf-single-sub-reflexive]
0	Thm* A:Type, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z Type	[fpf-cap-wf-univ]
0	Thm* eq:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v	[fpf-cap-single1]

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

mb event system 7 Sections EventSystems Doc