Nuprl - mb_event_system

Origin Definitions Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb_event_system_6Nuprl Section: mb_event_system_6

Selected Objects
def d-es es is an event system of D
== w:World, p:FairFifo. PossibleWorld(D;w) & es = ES(w)  ES

def d-realizes D
realizes es.P(es)
== D':Dsys. D  D'  (w:World, p:FairFifo. PossibleWorld(D';w)  P(ES(w)))

def d-realizes2 D realizes2 es.P(es) == w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w))

def msystem System == {M:(IdMsgA)| loc:Id. Feasible(M(loc)) }

def m-sys-at @i: A(j) == if j = i A else  fi

THM s-at-sub-s-at i:Id, A,B:MsgA. @i: A  @i: B  A  B

THM bool-inhabited

THM decidable-exists-finite P:(TProp). (x:T. Dec(P(x)))  finite-type(T)  Dec(x:T. P(x))

THM decidable__ex_unit P:(UnitProp). Dec(P())  Dec(x:Unit. P(x))

THM ma-empty-frame-compatible-left A:MsgA. ma-frame-compatible(; A)

THM ma-empty-sframe-compatible-right A:MsgA. ma-sframe-compatible(A; )

THM ma-empty-frame-compatible-right A:MsgA. ma-frame-compatible(A; )

THM ma-empty-sframe-compatible-left A:MsgA. ma-sframe-compatible(; A)

THM ma-compatible-join A,B,C:MsgA.
A || B

ma-frame-compatible(A; B)

ma-sframe-compatible(A; B)

C || A

ma-frame-compatible(C; A)

ma-sframe-compatible(C; A)

C || B

ma-frame-compatible(C; B)

ma-sframe-compatible(C; B)

C || A  B & ma-frame-compatible(C; A  B) & ma-sframe-compatible(C; A  B)

THM ma-compat-symmetry A,B:MsgA. A ||+ B  B ||+ A

THM ma-empty-compat-left A:MsgA.  ||+ A

THM ma-empty-compat-right A:MsgA. A ||+

THM ma-join-feasible A,B:MsgA.
A || B

ma-frame-compatible(A; B)

ma-sframe-compatible(A; B)  Feasible(A)  Feasible(B)  Feasible(A  B)

THM ma-compat-join A,B,C:MsgA. A ||+ B  C ||+ A  C ||+ B  C ||+ A  B

THM ma-join-list-property L:MsgA List.
(A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))

THM ma-sub-join-list L:MsgA List, M:MsgA. (A,BL.A ||+ B)  (M  L)  M  (L)

THM ma-join-list-feasible L:MsgA List. (A,BL.A ||+ B)  (AL.Feasible(A))  Feasible((L))

THM ma-join-list-compat L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.M ||+ B)  M ||+ (L))

THM ma-join-list-compat2 L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.B ||+ M)  (L) ||+ M)

THM msga-sub-msg-form MsgA r MsgAForm

THM msg-form-join A,B:MsgAForm. A  B  MsgAForm

THM msg-form-join-list L:MsgA List. (L)  MsgAForm

THM ma-join-list-is-empty L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)

THM assert-ma-join-list-is-empty L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L)

THM ma-outlinks-join A,B:MsgAForm, ltg:(IdLnkIdType), i:Id.
(ltg  ma-outlinks(A  B;i))

(ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i))

THM ma-outlinks-join-list L:MsgA List, P:(IdLnkIdTypeProp), i:Id.
(ML.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((L);i).P(ltg))

THM sub-join-list-din l:IdLnk, tg:Id, L:MsgA List. (ML.T r M.din(l,tg))  (T r (L).din(l,tg))

THM ma-single-pre-init1-feasible x:Id, c:T, a:Id, P:(TT'Prop).
T'

(u:T. Dec(v:T'. P(u,v)))

Feasible(ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)))

THM ma-single-effect-feasible x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
f:(State(ds)ma-valtype(da; k)ds(x)?Void).
xdom(ds). A=ds(x)   A

kdom(da). A=da(k)   A  Feasible(ma-single-effect(ds; da; k; x; f))

THM ma-single-effect0-feasible x:Id, k:Knd, A,T:Type, f:(ATA).
A  T  Feasible(ma-single-effect0(x;A;k;T;f))

THM ma-single-pre-feasible a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
T

xdom(ds). A=ds(x)   A

(s:State(ds). Dec(v:T. P(s,v)))

Feasible((with ds: ds
Faction a:T
Fprecondition a(v) is
FP s v))

THM ma-single-pre1-feasible a:Id, T,A:Type, x:Id, P:(ATProp).
T

A  (a:A. Dec(v:T. P(a,v)))  Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))

THM ma-single-sends-feasible k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
xdom(ds). A=ds(x)   A

kdom(da). A=da(k)   A  Feasible(ma-single-sends(ds; da; k; l; f))

THM d-sub_transitivity D1,D2,D3:Dsys. D1  D2  D2  D3  D1  D3

THM decidable__ma-decla A:Dsys, i,a:Id. Dec(a declared in M(i))

THM finite-support-feasible D:Dsys, L:Id List.
(i:Id. (i  L)  ma-is-empty(M(i)))

(i:Id. Feasible(M(i)))

(iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
(iL.(ltgma-outlinks(M(i);i).
interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))

d-feasible(D)

THM possible-world-monotonic A,B:Dsys. A  B  (w:World. PossibleWorld(B;w)  PossibleWorld(A;w))

THM d-realizes2-implies-realizes D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
D realizes2 es.P(es)  D realizes es.P(es)

THM realizes-monotone-wrt-sub D,D':Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
D realizes es.P(es)  D  D'  D' realizes es.P(es)

THM init-rule i:Id, T:Type, v:T, x:Id.
@i: x:T
@i: xinitially x = v
realizes es.(vartype(i;x) r T)
realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T)

THM frame-rule i:Id, L:Knd List, x:Id, T:Type.
@i: only L affects x : T
realizes es.(vartype(i;x) r T)
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id
realizes es.& (
realizes es.& (((x after e) = (x when e)  T  (kind(e)  L))
realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T))

THM sframe-rule i:Id, L:Knd List, l:IdLnk, tg:Id.
@i: only L sends on (l with tg)
realizes es.e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)

THM effect-rule i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
f:(State(ds)ma-valtype(da; k)ds(x)?Void).
d-single-effect(i; ds; da; k; x; f)
realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
realizes es.& (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id
realizes es.& (
realizes es.& (kind(e) = k  Knd
realizes es.& (
realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top)

THM sends-rule i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
source(l) = i

d-single-sends(i; ds; da; k; l; f)
realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
realizes es.& (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
realizes es.& (e:E.
realizes es.& (isrcv(e)
realizes es.& (
realizes es.& (lnk(e) = l  IdLnk  (valtype(e) r ma-valtype(da; kind(e))))
realizes es.& ({m:Msg| source(mlnk(m)) = i } r Msg
realizes es.& (((l,tg. da(rcv(l; tg))?Top)))
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id
realizes es.& (
realizes es.& (kind(e) = k  Knd
realizes es.& (
realizes es.& (sends(l;e)
realizes es.& (=
realizes es.& (tagged-messages(l;z.(z when e);val(e);f)
realizes es.& ( Msg((l,tg. da(rcv(l; tg))?Top)) List)

THM better-sends-rule i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
source(l) = i

d-single-sends(i; ds; da; k; l; f)
realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
realizes es.& (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
realizes es.& (e:E.
realizes es.& (isrcv(e)
realizes es.& (
realizes es.& (lnk(e) = l  IdLnk  (valtype(e) r ma-valtype(da; kind(e))))
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id
realizes es.& (
realizes es.& (kind(e) = k  Knd
realizes es.& (
realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
realizes es.& (((e':E.
realizes es.& ((((e'  L)
realizes es.& (((
realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
realizes es.& ((& =
realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List))

THM pre-rule i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
@i (with ds: ds
@i action a:T
@i precondition a(v) is
@i P s v)
realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id  kind(e) = locl(a)  Knd  (valtype(e) r T))
realizes es.& (e:E.
realizes es.& (loc(e) = i  Id
realizes es.& (
realizes es.& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e)))
realizes es.& (& (e':E.
realizes es.& (& ((e <loc e')  e = e'  E
realizes es.& (& (& kind(e') = locl(a)  Knd  (v:T. P((z.(z after e')),v))))

THM pre-init-rule i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp),
init:x:Id fp-> ds(x)?Void.
(x:Id. x  dom(ds)  x  dom(init))

@i (with ds: ds
@i init: init
@i action a:T
@i precondition a(v) is
@i P s v)
realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)

THM s-pre-init-rule i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp),
init:x:Id fp-> ds(x)?Void.
(x:Id. x  dom(ds)  x  dom(init))

@i: (with ds: ds init: initaction a:T precondition a(v) is P)  Dsys
& (D:Dsys.
& (@i: (with ds: ds
& (@init: init
& (action a:T
& (aprecondition a(v) is
& (aP)  D
& (
& (D
& (realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id))

THM s-pre-rule i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp).
@i: (with ds: ds action a:T precondition a(v) is P s v)  Dsys
& (D:Dsys.
& (@i: (with ds: ds
& (@action a:T
& (@precondition a(v) is
& (@P s v)  D
& (
& (D
& (realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e)))
& (realizes es.& (& (e':E.
& (realizes es.& (& ((e <loc e')  e = e'  E
& (realizes es.& (& (& kind(e') = locl(a)  Knd
& (realizes es.& (& (&  (v:T. P((z.(z after e')),v)))))

THM s-pre-rule1 i,a,x:Id, A,T:Type, P:(ATProp).
@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys
& (D:Dsys.
& (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D
& (
& (D
& (realizes es.(vartype(i;x) r A)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& ((kind(e) = locl(a)  Knd  P((x when e),val(e)))
& (realizes es.& (& (e':E.
& (realizes es.& (& ((e <loc e')  e = e'  E
& (realizes es.& (& (& kind(e') = locl(a)  Knd  (v:T. P((x after e'),v)))))

THM s-effect-rule i,x:Id, k:Knd, ds:a:Id fp-> Type, da:a:Knd fp-> Type,
f:(State(ds)ma-valtype(da; k)ds(x)?Void).
@i: ma-single-effect(ds; da; k; x; f)  Dsys
& (D:Dsys.
& (@i: ma-single-effect(ds; da; k; x; f)  D
& (
& (D
& (realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = k  Knd
& (realizes es.& (
& (realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top))

THM s-effect-rule0 i,x:Id, a:Knd, T,A:Type, f:(ATA).
@i: ma-single-effect0(x;A;a;T;f)  Dsys
& (D:Dsys.
& (@i: ma-single-effect0(x;A;a;T;f)  D
& (
& (D
& (realizes es.(vartype(i;x) r A)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id  kind(e) = a  Knd  (valtype(e) r T))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = a  Knd  (x after e) = f((x when e),val(e))  A))

THM effect-rule1 i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA).
y = x

@i: ma-single-effect1(x;A;y;B;k;T;f)  Dsys
& (D:Dsys.
& (@i: ma-single-effect1(x;A;y;B;k;T;f)  D
& (
& (D
& (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = k  Knd
& (realizes es.& (
& (realizes es.& ((x after e) = f((x when e),(y when e),val(e))  A))

THM s-sends-rule i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type,
f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
source(l) = i

@i: ma-single-sends(ds; da; k; l; f)  Dsys
& (D:Dsys.
& (@i: ma-single-sends(ds; da; k; l; f)  D
& (
& (D
& (realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
& (realizes es.& (e:E.
& (realizes es.& (isrcv(e)
& (realizes es.& (
& (realizes es.& (lnk(e) = l  IdLnk  (valtype(e) r ma-valtype(da; kind(e))))
& (realizes es.& (e:E.
& (realizes es.& (loc(e) = i  Id
& (realizes es.& (
& (realizes es.& (kind(e) = k  Knd
& (realizes es.& (
& (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
& (realizes es.& (((e':E.
& (realizes es.& ((((e'  L)
& (realizes es.& (((
& (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
& (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
& (realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
& (realizes es.& ((& =
& (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
& (realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List)))

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

Selected Objects
def	d-es	es is an event system of D == w:World, p:FairFifo. PossibleWorld(D;w) & es = ES(w) ES
def	d-realizes	D realizes es.P(es) == D':Dsys. D D' (w:World, p:FairFifo. PossibleWorld(D';w) P(ES(w)))
def	d-realizes2	D realizes2 es.P(es) == w:World, p:FairFifo. PossibleWorld(D;w) P(ES(w))
def	msystem	System == {M:(IdMsgA)\| loc:Id. Feasible(M(loc)) }
def	m-sys-at	@i: A(j) == if j = i A else fi
THM	s-at-sub-s-at	i:Id, A,B:MsgA. @i: A @i: B A B
THM	bool-inhabited
THM	decidable-exists-finite	P:(TProp). (x:T. Dec(P(x))) finite-type(T) Dec(x:T. P(x))
THM	decidable__ex_unit	P:(UnitProp). Dec(P()) Dec(x:Unit. P(x))
THM	ma-empty-frame-compatible-left	A:MsgA. ma-frame-compatible(; A)
THM	ma-empty-sframe-compatible-right	A:MsgA. ma-sframe-compatible(A; )
THM	ma-empty-frame-compatible-right	A:MsgA. ma-frame-compatible(A; )
THM	ma-empty-sframe-compatible-left	A:MsgA. ma-sframe-compatible(; A)
THM	ma-compatible-join	A,B,C:MsgA. A \|\| B ma-frame-compatible(A; B) ma-sframe-compatible(A; B) C \|\| A ma-frame-compatible(C; A) ma-sframe-compatible(C; A) C \|\| B ma-frame-compatible(C; B) ma-sframe-compatible(C; B) C \|\| A B & ma-frame-compatible(C; A B) & ma-sframe-compatible(C; A B)
THM	ma-compat-symmetry	A,B:MsgA. A \|\|+ B B \|\|+ A
THM	ma-empty-compat-left	A:MsgA. \|\|+ A
THM	ma-empty-compat-right	A:MsgA. A \|\|+
THM	ma-join-feasible	A,B:MsgA. A \|\| B ma-frame-compatible(A; B) ma-sframe-compatible(A; B) Feasible(A) Feasible(B) Feasible(A B)
THM	ma-compat-join	A,B,C:MsgA. A \|\|+ B C \|\|+ A C \|\|+ B C \|\|+ A B
THM	ma-join-list-property	L:MsgA List. (A,BL.A \|\|+ B) (L) MsgA & (M:MsgA. (BL.M \|\|+ B) M \|\|+ (L))
THM	ma-sub-join-list	L:MsgA List, M:MsgA. (A,BL.A \|\|+ B) (M L) M (L)
THM	ma-join-list-feasible	L:MsgA List. (A,BL.A \|\|+ B) (AL.Feasible(A)) Feasible((L))
THM	ma-join-list-compat	L:MsgA List. (A,BL.A \|\|+ B) (M:MsgA. (BL.M \|\|+ B) M \|\|+ (L))
THM	ma-join-list-compat2	L:MsgA List. (A,BL.A \|\|+ B) (M:MsgA. (BL.B \|\|+ M) (L) \|\|+ M)
THM	msga-sub-msg-form	MsgA r MsgAForm
THM	msg-form-join	A,B:MsgAForm. A B MsgAForm
THM	msg-form-join-list	L:MsgA List. (L) MsgAForm
THM	ma-join-list-is-empty	L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)
THM	assert-ma-join-list-is-empty	L:MsgA List. ma-is-empty((L)) reduce(M,x. ma-is-empty(M) & x;True;L)
THM	ma-outlinks-join	A,B:MsgAForm, ltg:(IdLnkIdType), i:Id. (ltg ma-outlinks(A B;i)) (ltg ma-outlinks(A;i)) (ltg ma-outlinks(B;i))
THM	ma-outlinks-join-list	L:MsgA List, P:(IdLnkIdTypeProp), i:Id. (ML.(ltgma-outlinks(M;i).P(ltg))) (ltgma-outlinks((L);i).P(ltg))
THM	sub-join-list-din	l:IdLnk, tg:Id, L:MsgA List. (ML.T r M.din(l,tg)) (T r (L).din(l,tg))
THM	ma-single-pre-init1-feasible	x:Id, c:T, a:Id, P:(TT'Prop). T' (u:T. Dec(v:T'. P(u,v))) Feasible(ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)))
THM	ma-single-effect-feasible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(State(ds)ma-valtype(da; k)ds(x)?Void). xdom(ds). A=ds(x) A kdom(da). A=da(k) A Feasible(ma-single-effect(ds; da; k; x; f))
THM	ma-single-effect0-feasible	x:Id, k:Knd, A,T:Type, f:(ATA). A T Feasible(ma-single-effect0(x;A;k;T;f))
THM	ma-single-pre-feasible	a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). T xdom(ds). A=ds(x) A (s:State(ds). Dec(v:T. P(s,v))) Feasible((with ds: ds Faction a:T Fprecondition a(v) is FP s v))
THM	ma-single-pre1-feasible	a:Id, T,A:Type, x:Id, P:(ATProp). T A (a:A. Dec(v:T. P(a,v))) Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))
THM	ma-single-sends-feasible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. xdom(ds). A=ds(x) A kdom(da). A=da(k) A Feasible(ma-single-sends(ds; da; k; l; f))
THM	d-sub_transitivity	D1,D2,D3:Dsys. D1 D2 D2 D3 D1 D3
THM	decidable__ma-decla	A:Dsys, i,a:Id. Dec(a declared in M(i))
THM	finite-support-feasible	D:Dsys, L:Id List. (i:Id. (i L) ma-is-empty(M(i))) (i:Id. Feasible(M(i))) (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg)) L) (iL.(ltgma-outlinks(M(i);i). interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg))))) d-feasible(D)
THM	possible-world-monotonic	A,B:Dsys. A B (w:World. PossibleWorld(B;w) PossibleWorld(A;w))
THM	d-realizes2-implies-realizes	D:Dsys, P:({es:ES\| es is an event system of D }Prop{i'}). D realizes2 es.P(es) D realizes es.P(es)
THM	realizes-monotone-wrt-sub	D,D':Dsys, P:({es:ES\| es is an event system of D }Prop{i'}). D realizes es.P(es) D D' D' realizes es.P(es)
THM	init-rule	i:Id, T:Type, v:T, x:Id. @i: x:T @i: xinitially x = v realizes es.(vartype(i;x) r T) realizes es.& (e:E. loc(e) = i Id first(e) (x when e) = v T)
THM	frame-rule	i:Id, L:Knd List, x:Id, T:Type. @i: only L affects x : T realizes es.(vartype(i;x) r T) realizes es.& (e:E. realizes es.& (loc(e) = i Id realizes es.& ( realizes es.& (((x after e) = (x when e) T (kind(e) L)) realizes es.& (& ((kind(e) L) (x after e) = (x when e) T))
THM	sframe-rule	i:Id, L:Knd List, l:IdLnk, tg:Id. @i: only L sends on (l with tg) realizes es.e:E. loc(e) = i Id null(sends(l,tg,e)) (kind(e) L)
THM	effect-rule	i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(State(ds)ma-valtype(da; k)ds(x)?Void). d-single-effect(i; ds; da; k; x; f) realizes es.(x:Id. vartype(i;x) r ds(x)?Top) realizes es.& (e:E. loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) realizes es.& (e:E. realizes es.& (loc(e) = i Id realizes es.& ( realizes es.& (kind(e) = k Knd realizes es.& ( realizes es.& ((x after e) = f((z.(z when e)),val(e)) ds(x)?Top)
THM	sends-rule	i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. source(l) = i d-single-sends(i; ds; da; k; l; f) realizes es.(x:Id. vartype(i;x) r ds(x)?Top) realizes es.& (e:E. loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) realizes es.& (e:E. realizes es.& (isrcv(e) realizes es.& ( realizes es.& (lnk(e) = l IdLnk (valtype(e) r ma-valtype(da; kind(e)))) realizes es.& ({m:Msg\| source(mlnk(m)) = i } r Msg realizes es.& (((l,tg. da(rcv(l; tg))?Top))) realizes es.& (e:E. realizes es.& (loc(e) = i Id realizes es.& ( realizes es.& (kind(e) = k Knd realizes es.& ( realizes es.& (sends(l;e) realizes es.& (= realizes es.& (tagged-messages(l;z.(z when e);val(e);f) realizes es.& ( Msg((l,tg. da(rcv(l; tg))?Top)) List)
THM	better-sends-rule	i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. source(l) = i d-single-sends(i; ds; da; k; l; f) realizes es.(x:Id. vartype(i;x) r ds(x)?Top) realizes es.& (e:E. loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) realizes es.& (e:E. realizes es.& (isrcv(e) realizes es.& ( realizes es.& (lnk(e) = l IdLnk (valtype(e) r ma-valtype(da; kind(e)))) realizes es.& (e:E. realizes es.& (loc(e) = i Id realizes es.& ( realizes es.& (kind(e) = k Knd realizes es.& ( realizes es.& ((L:{e':E\| isrcv(e') & lnk(e') = l IdLnk } List. realizes es.& (((e':E. realizes es.& ((((e' L) realizes es.& ((( realizes es.& (((isrcv(e') & lnk(e') = l IdLnk & sender(e') = e E) realizes es.& ((& (e1,e2:E. e1 before e2 L (e1 <loc e2)) realizes es.& ((& map(e'.<tag(e'),val(e')>;L) realizes es.& ((& = realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) realizes es.& ((& (tg:Idma-valtype(da; rcv(l; tg))) List))
THM	pre-rule	i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). @i (with ds: ds @i action a:T @i precondition a(v) is @i P s v) realizes es.(x:Id. vartype(i;x) r ds(x)?Top) realizes es.& (e:E. realizes es.& (loc(e) = i Id kind(e) = locl(a) Knd (valtype(e) r T)) realizes es.& (e:E. realizes es.& (loc(e) = i Id realizes es.& ( realizes es.& ((kind(e) = locl(a) Knd P((z.(z when e)),val(e))) realizes es.& (& (e':E. realizes es.& (& ((e <loc e') e = e' E realizes es.& (& (& kind(e') = locl(a) Knd (v:T. P((z.(z after e')),v))))
THM	pre-init-rule	i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp), init:x:Id fp-> ds(x)?Void. (x:Id. x dom(ds) x dom(init)) @i (with ds: ds @i init: init @i action a:T @i precondition a(v) is @i P s v) realizes es.(v:T. P((x.init(x)?),v)) (e:E. loc(e) = i Id)
THM	s-pre-init-rule	i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp), init:x:Id fp-> ds(x)?Void. (x:Id. x dom(ds) x dom(init)) @i: (with ds: ds init: initaction a:T precondition a(v) is P) Dsys & (D:Dsys. & (@i: (with ds: ds & (@init: init & (action a:T & (aprecondition a(v) is & (aP) D & ( & (D & (realizes es.(v:T. P((x.init(x)?),v)) (e:E. loc(e) = i Id))
THM	s-pre-rule	i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp). @i: (with ds: ds action a:T precondition a(v) is P s v) Dsys & (D:Dsys. & (@i: (with ds: ds & (@action a:T & (@precondition a(v) is & (@P s v) D & ( & (D & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = locl(a) Knd (valtype(e) r T)) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& ((kind(e) = locl(a) Knd P((z.(z when e)),val(e))) & (realizes es.& (& (e':E. & (realizes es.& (& ((e <loc e') e = e' E & (realizes es.& (& (& kind(e') = locl(a) Knd & (realizes es.& (& (& (v:T. P((z.(z after e')),v)))))
THM	s-pre-rule1	i,a,x:Id, A,T:Type, P:(ATProp). @i: ma-single-pre1(x;A;a;T;x,v.P(x,v)) Dsys & (D:Dsys. & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v)) D & ( & (D & (realizes es.(vartype(i;x) r A) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = locl(a) Knd (valtype(e) r T)) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& ((kind(e) = locl(a) Knd P((x when e),val(e))) & (realizes es.& (& (e':E. & (realizes es.& (& ((e <loc e') e = e' E & (realizes es.& (& (& kind(e') = locl(a) Knd (v:T. P((x after e'),v)))))
THM	s-effect-rule	i,x:Id, k:Knd, ds:a:Id fp-> Type, da:a:Knd fp-> Type, f:(State(ds)ma-valtype(da; k)ds(x)?Void). @i: ma-single-effect(ds; da; k; x; f) Dsys & (D:Dsys. & (@i: ma-single-effect(ds; da; k; x; f) D & ( & (D & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = k Knd & (realizes es.& ( & (realizes es.& ((x after e) = f((z.(z when e)),val(e)) ds(x)?Top))
THM	s-effect-rule0	i,x:Id, a:Knd, T,A:Type, f:(ATA). @i: ma-single-effect0(x;A;a;T;f) Dsys & (D:Dsys. & (@i: ma-single-effect0(x;A;a;T;f) D & ( & (D & (realizes es.(vartype(i;x) r A) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id kind(e) = a Knd (valtype(e) r T)) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = a Knd (x after e) = f((x when e),val(e)) A))
THM	effect-rule1	i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA). y = x @i: ma-single-effect1(x;A;y;B;k;T;f) Dsys & (D:Dsys. & (@i: ma-single-effect1(x;A;y;B;k;T;f) D & ( & (D & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id kind(e) = k Knd (valtype(e) r T)) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = k Knd & (realizes es.& ( & (realizes es.& ((x after e) = f((x when e),(y when e),val(e)) A))
THM	s-sends-rule	i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type, f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. source(l) = i @i: ma-single-sends(ds; da; k; l; f) Dsys & (D:Dsys. & (@i: ma-single-sends(ds; da; k; l; f) D & ( & (D & (realizes es.(x:Id. vartype(i;x) r ds(x)?Top) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) & (realizes es.& (e:E. & (realizes es.& (isrcv(e) & (realizes es.& ( & (realizes es.& (lnk(e) = l IdLnk (valtype(e) r ma-valtype(da; kind(e)))) & (realizes es.& (e:E. & (realizes es.& (loc(e) = i Id & (realizes es.& ( & (realizes es.& (kind(e) = k Knd & (realizes es.& ( & (realizes es.& ((L:{e':E\| isrcv(e') & lnk(e') = l IdLnk } List. & (realizes es.& (((e':E. & (realizes es.& ((((e' L) & (realizes es.& ((( & (realizes es.& (((isrcv(e') & lnk(e') = l IdLnk & sender(e') = e E) & (realizes es.& ((& (e1,e2:E. e1 before e2 L (e1 <loc e2)) & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L) & (realizes es.& ((& = & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) & (realizes es.& ((& (tg:Idma-valtype(da; rcv(l; tg))) List)))

Origin Definitions Sections EventSystems Doc