Nuprl - mb_event_system_6 Citations of Knd

mb event system 6 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Knd == (IdLnk

Id)+Id

is mentioned by

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
Thm* source(l) = i
Thm*
Thm* @i: ma-single-sends(ds; da; k; l; f)  Dsys
Thm* & (D:Dsys.
Thm* & (@i: ma-single-sends(ds; da; k; l; 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.& (isrcv(e)
Thm* & (realizes es.& (
Thm* & (realizes es.& (lnk(e) = l  IdLnk
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.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
Thm* & (realizes es.& (((e':E.
Thm* & (realizes es.& ((((e'  L)
Thm* & (realizes es.& (((
Thm* & (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
Thm* & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
Thm* & (realizes es.& ((& =
Thm* & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
Thm* & (realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List))) [s-sends-rule]

Thm* i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA).
Thm* y = x
Thm*
Thm* @i: ma-single-effect1(x;A;y;B;k;T;f)  Dsys
Thm* & (D:Dsys.
Thm* & (@i: ma-single-effect1(x;A;y;B;k;T;f)  D
Thm* & (
Thm* & (D
Thm* & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B)
Thm* & (realizes es.& (e:E.
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = k  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) = k  Knd
Thm* & (realizes es.& (
Thm* & (realizes es.& ((x after e) = f((x when e),(y when e),val(e))  A)) [effect-rule1]

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]

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]

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]

Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp).
Thm* @i: (with ds: ds action a:T precondition a(v) is P s v)  Dsys
Thm* & (D:Dsys.
Thm* & (@i: (with ds: ds
Thm* & (@action a:T
Thm* & (@precondition a(v) is
Thm* & (@P s v)  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.& (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((z.(z 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((z.(z after e')),v))))) [s-pre-rule]

Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
Thm* @i (with ds: ds
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v)
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.& (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((z.(z 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((z.(z after e')),v)))) [pre-rule]

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
Thm* source(l) = i
Thm*
Thm* d-single-sends(i; ds; da; k; l; f)
Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
Thm* realizes es.& (e:E.
Thm* realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E.
Thm* realizes es.& (isrcv(e)
Thm* realizes es.& (
Thm* realizes es.& (lnk(e) = l  IdLnk
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.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
Thm* realizes es.& (((e':E.
Thm* realizes es.& ((((e'  L)
Thm* realizes es.& (((
Thm* realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
Thm* realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
Thm* realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
Thm* realizes es.& ((& =
Thm* realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
Thm* realizes es.& ((&  (tg:Idma-valtype(da; rcv(l; tg))) List)) [better-sends-rule]

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
Thm* source(l) = i
Thm*
Thm* d-single-sends(i; ds; da; k; l; f)
Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
Thm* realizes es.& (e:E.
Thm* realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E.
Thm* realizes es.& (isrcv(e)
Thm* realizes es.& (
Thm* realizes es.& (lnk(e) = l  IdLnk
Thm* realizes es.& (
Thm* realizes es.& ((valtype(e) r ma-valtype(da; kind(e))))
Thm* realizes es.& ({m:Msg| source(mlnk(m)) = i } r Msg
Thm* realizes es.& (((l,tg. da(rcv(l; tg))?Top)))
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.& (sends(l;e)
Thm* realizes es.& (=
Thm* realizes es.& (tagged-messages(l;z.(z when e);val(e);f)
Thm* realizes es.& ( Msg((l,tg. da(rcv(l; tg))?Top)) List) [sends-rule]

Thm* i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void).
Thm* d-single-effect(i; ds; da; k; x; f)
Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
Thm* realizes es.& (e:E.
Thm* realizes es.& (loc(e) = i  Id  (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) [effect-rule]

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

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]

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

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

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

Thm* A,B,T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(AB(T List)).
Thm* (a = rcv(l; tg)  T = B)
Thm*
Thm* ma-single-sends1(A; B; T; x; a; l; tg; f)  MsgA [ma-single-sends1_wf]

In prior sections: mb event system 1 mb event system 2 mb event system 3 mb event system 4 mb event system 5

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 6 Sections EventSystems Doc

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm* Thm* @i: ma-single-sends(ds; da; k; l; f) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-sends(ds; da; k; l; 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.& (isrcv(e) Thm* & (realizes es.& ( Thm* & (realizes es.& (lnk(e) = l IdLnk 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.& ((L:{e':E\| isrcv(e') & lnk(e') = l IdLnk } List. Thm* & (realizes es.& (((e':E. Thm* & (realizes es.& ((((e' L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((isrcv(e') & lnk(e') = l IdLnk & sender(e') = e E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2 L (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L) Thm* & (realizes es.& ((& = Thm* & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) Thm* & (realizes es.& ((& (tg:Idma-valtype(da; rcv(l; tg))) List)))	[s-sends-rule]
Thm* i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA). Thm* y = x Thm* Thm* @i: ma-single-effect1(x;A;y;B;k;T;f) Dsys Thm* & (D:Dsys. Thm* & (@i: ma-single-effect1(x;A;y;B;k;T;f) D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B) Thm* & (realizes es.& (e:E. Thm* & (realizes es.& (loc(e) = i Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k 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) = k Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((x after e) = f((x when e),(y when e),val(e)) A))	[effect-rule1]
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]
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]
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]
Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp). Thm* @i: (with ds: ds action a:T precondition a(v) is P s v) Dsys Thm* & (D:Dsys. Thm* & (@i: (with ds: ds Thm* & (@action a:T Thm* & (@precondition a(v) is Thm* & (@P s v) 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.& (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((z.(z 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((z.(z after e')),v)))))	[s-pre-rule]
Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* @i (with ds: ds Thm* @i action a:T Thm* @i precondition a(v) is Thm* @i P s v) 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.& (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((z.(z 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((z.(z after e')),v))))	[pre-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm* Thm* d-single-sends(i; ds; da; k; l; f) Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E. Thm* realizes es.& (loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E. Thm* realizes es.& (isrcv(e) Thm* realizes es.& ( Thm* realizes es.& (lnk(e) = l IdLnk 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.& ((L:{e':E\| isrcv(e') & lnk(e') = l IdLnk } List. Thm* realizes es.& (((e':E. Thm* realizes es.& ((((e' L) Thm* realizes es.& ((( Thm* realizes es.& (((isrcv(e') & lnk(e') = l IdLnk & sender(e') = e E) Thm* realizes es.& ((& (e1,e2:E. e1 before e2 L (e1 <loc e2)) Thm* realizes es.& ((& map(e'.<tag(e'),val(e')>;L) Thm* realizes es.& ((& = Thm* realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f) Thm* realizes es.& ((& (tg:Idma-valtype(da; rcv(l; tg))) List))	[better-sends-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* source(l) = i Thm* Thm* d-single-sends(i; ds; da; k; l; f) Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E. Thm* realizes es.& (loc(e) = i Id (valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E. Thm* realizes es.& (isrcv(e) Thm* realizes es.& ( Thm* realizes es.& (lnk(e) = l IdLnk Thm* realizes es.& ( Thm* realizes es.& ((valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& ({m:Msg\| source(mlnk(m)) = i } r Msg Thm* realizes es.& (((l,tg. da(rcv(l; tg))?Top))) 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.& (sends(l;e) Thm* realizes es.& (= Thm* realizes es.& (tagged-messages(l;z.(z when e);val(e);f) Thm* realizes es.& ( Msg((l,tg. da(rcv(l; tg))?Top)) List)	[sends-rule]
Thm* i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* d-single-effect(i; ds; da; k; x; f) Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E. Thm* realizes es.& (loc(e) = i Id (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)	[effect-rule]
Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg) Thm* realizes es.e:E. loc(e) = i Id null(sends(l,tg,e)) (kind(e) L)	[sframe-rule]
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]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List. Thm* xdom(ds). A=ds(x) A Thm* Thm* kdom(da). A=da(k) A Feasible(ma-single-sends(ds; da; k; l; f))	[ma-single-sends-feasible]
Thm* x:Id, k:Knd, A,T:Type, f:(ATA). Thm* A T Feasible(ma-single-effect0(x;A;k;T;f))	[ma-single-effect0-feasible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* xdom(ds). A=ds(x) A Thm* Thm* kdom(da). A=da(k) A Feasible(ma-single-effect(ds; da; k; x; f))	[ma-single-effect-feasible]
Thm* A,B,T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(AB(T List)). Thm* (a = rcv(l; tg) T = B) Thm* Thm* ma-single-sends1(A; B; T; x; a; l; tg; f) MsgA	[ma-single-sends1_wf]