Nuprl - mb_event_system_7 Citations of ma-single-sframe

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)

is mentioned by

Thm* l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top.
Thm* x : t initially x = v ||+ only L sends on (l with tg) [ma-single-init-ma-single-sframe-compatible]

Thm* l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top.
Thm* only members of L1 affect x :t ||+ only L sends on (l with tg) [ma-single-frame-ma-single-sframe-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Top, da:a:Knd fp-> Top, f:Top, l:IdLnk, tg:Id,
Thm* L:Top. ma-single-effect(ds; da; k; x; f) ||+ only L sends on (l with tg) [ma-single-effect-ma-single-sframe-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* l1:IdLnk, tg:Id, L:Knd List.
Thm* (l = l1  (tg  map(p.1of(p);f))  (k  L))
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ only L sends on (l1 with tg) [ma-single-sends-ma-single-sframe-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Top, P:Top, l:IdLnk, tg:Id, L:Top.
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ only L sends on (l with tg) [ma-single-pre-ma-single-sframe-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id,
Thm* L:Knd List.
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ only L sends on (l with tg) [ma-single-pre-init-ma-single-sframe-compatible]

Thm* L:Knd List, l:IdLnk, tg:Id.
Thm* @source(l): only L sends on (l with tg)  Dsys
Thm* & (D:Dsys.
Thm* & (@source(l): only L sends on (l with tg)  D
Thm* & (
Thm* & (D
Thm* & (realizes es.e:E.
Thm* & (realizes es.loc(e) = destination(l)  Id
Thm* & (realizes es.
Thm* & (realizes es.kind(e) = rcv(l; tg)  Knd  (kind(sender(e))  L)) [better-sframe-rule]

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

Def ring-leader1(loc;R;uid;out;in)
Def == if R(loc)
Def == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me"));
Def == if [(trigger1(loc;;;x,y. x=y;loc;rcv
Def == if [((in(loc)); "vote");"leader";"me"));
Def == if [(Dconstant(loc;;uid(loc);"me";loc));
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1("me";
Def == if [ma-single-sends1(rcv((in(loc)); "vote");
Def == if [ma-single-sends1((out(loc));
Def == if [ma-single-sends1("vote";
Def == if [ma-single-sends1((a,b. if a<b [b] else nil fi));
Def == if [only [rcv((in(loc)); "vote");
Def == if [only [locl("send-me")] sends on (out(loc) with "vote")]
Def == else nil fi [ring-leader1]

In prior sections: 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 7 Sections EventSystems Doc

Thm* l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top. Thm* x : t initially x = v \|\|+ only L sends on (l with tg)	[ma-single-init-ma-single-sframe-compatible]
Thm* l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top. Thm* only members of L1 affect x :t \|\|+ only L sends on (l with tg)	[ma-single-frame-ma-single-sframe-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Top, da:a:Knd fp-> Top, f:Top, l:IdLnk, tg:Id, Thm* L:Top. ma-single-effect(ds; da; k; x; f) \|\|+ only L sends on (l with tg)	[ma-single-effect-ma-single-sframe-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* l1:IdLnk, tg:Id, L:Knd List. Thm* (l = l1 (tg map(p.1of(p);f)) (k L)) Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ only L sends on (l1 with tg)	[ma-single-sends-ma-single-sframe-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Top, P:Top, l:IdLnk, tg:Id, L:Top. Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ only L sends on (l with tg)	[ma-single-pre-ma-single-sframe-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id, Thm* L:Knd List. Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ only L sends on (l with tg)	[ma-single-pre-init-ma-single-sframe-compatible]
Thm* L:Knd List, l:IdLnk, tg:Id. Thm* @source(l): only L sends on (l with tg) Dsys Thm* & (D:Dsys. Thm* & (@source(l): only L sends on (l with tg) D Thm* & ( Thm* & (D Thm* & (realizes es.e:E. Thm* & (realizes es.loc(e) = destination(l) Id Thm* & (realizes es. Thm* & (realizes es.kind(e) = rcv(l; tg) Knd (kind(sender(e)) L))	[better-sframe-rule]
Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg) Dsys Thm* & (D:Dsys. Thm* & (@i: only L sends on (l with tg) D Thm* & ( Thm* & (D Thm* & (realizes es.e:E. Thm* & (realizes es.loc(e) = i Id null(sends(l,tg,e)) (kind(e) L))	[s-sframe-rule]
Def ring-leader1(loc;R;uid;out;in) Def == if R(loc) Def == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me")); Def == if [(trigger1(loc;;;x,y. x=y;loc;rcv Def == if [((in(loc)); "vote");"leader";"me")); Def == if [(Dconstant(loc;;uid(loc);"me";loc)); Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1(; Def == if [ma-single-sends1("me"; Def == if [ma-single-sends1(rcv((in(loc)); "vote"); Def == if [ma-single-sends1((out(loc)); Def == if [ma-single-sends1("vote"; Def == if [ma-single-sends1((a,b. if a<b [b] else nil fi)); Def == if [only [rcv((in(loc)); "vote"); Def == if [only [locl("send-me")] sends on (out(loc) with "vote")] Def == else nil fi	[ring-leader1]