Nuprl - mb_event_system_7 Citations of locl

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def locl(a) == inr(a)

is mentioned by

Thm* R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|; ; uid)
Thm*
Thm* loc.(ring-leader1(loc;R;uid;out;in))
Thm* realizes es.ldr:|R|.
Thm* realizes es.e@ldr.kind(e) = locl("leader")
Thm* realizes es.& (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|) [ring-leader1__realizes]

Thm* P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = "trigger"
Thm*
Thm* locl(a) = k
Thm*
Thm* loc.(trigger1(loc;T;A;P;i;k;a;x))
Thm* realizes es.(vartype(i;x) r A)
Thm* realizes es.& e@i.kind(e) = k  Knd  (valtype(e) r T)
Thm* realizes es.& e'@i.kind(e') = locl(a)
Thm* realizes es.& e'@i.
Thm* realizes es.& (e:E.
Thm* realizes es.& ((e <loc e') & kind(e) = k  Knd & P((x when e),val(e)))
Thm* realizes es.& e@i.kind(e) = k  Knd
Thm* realizes es.& e@i.
Thm* realizes es.& P((x when e),val(e))  e'@i.kind(e') = locl(a)  Knd [trigger1__realizes]

Thm* P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = "trigger"
Thm*
Thm* locl(a) = k  d-feasible(loc.(trigger1(loc;T;A;P;i;k;a;x))) [trigger1__feasible]

Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = "trigger"  locl(a) = k  trigger1(loc;T;A;P;i;k;a;x)  MsgA List [trigger1_wf]

Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = "trigger"
Thm*
Thm* locl(a) = k  (A,Btrigger1(loc;T;A;P;i;k;a;x).A ||+ B) [trigger1__compatible]

Thm* a:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x
Thm*
Thm* A
Thm*
Thm* T
Thm*
Thm* loc.(send-once(loc;T;A;a;f;tg;l;x))
Thm* realizes es.(vartype(source(l);x) r A)
Thm* realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T))
Thm* realizes es.& (e:E.
Thm* realizes es.& (kind(e) = rcv(l; tg)  Knd
Thm* realizes es.& (& val(e) = f((x when sender(e)))  T
Thm* realizes es.& (& & kind(sender(e)) = locl(a)  Knd
Thm* realizes es.& (& & (e':E.
Thm* realizes es.& (& & (kind(e') = rcv(l; tg)  Knd
Thm* realizes es.& (& & (
Thm* realizes es.& (& & (kind(sender(e')) = locl(a)  Knd  e' = e  E)) [send-once__realizes]

Thm* a,i:Id.
Thm* loc.(once(loc;a;i))
Thm* realizes es.e@i.kind(e) = locl(a)
Thm* realizes es.& e@i.e'@i.kind(e) = locl(a)
Thm* realizes es.& e@i.e'@i.
Thm* realizes es.& kind(e') = locl(a)  Knd  e = e'  E [once__realizes]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* ma-single-effect(d1; da; k; x; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v) [ma-single-effect-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* ma-single-sends(d1; da; k; l; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v) [ma-single-sends-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ ma-single-sends(d1; da; k; l; f) [ma-single-pre-ma-single-sends-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd,
Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-effect(d1; da; k; x; f) [ma-single-pre-init-ma-single-effect-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd,
Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-sends(d1; da; k; l; f) [ma-single-pre-init-ma-single-sends-compatible]

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]

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]

Def send-once(loc;T;A;a;f;tg;l;x)
Def == [(once(loc;a;source(l)));
Def == [if loc = source(l)
Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))]))
Def == [else  fi] [send-once]

Def once(loc;a;i)
Def == if loc = i
Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);
Def == if [only members of [locl(a)] affect "done" :;
Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)]
Def == else nil fi [once]

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

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* R:(Id), uid:(\|R\|), out,in:(\|R\|IdLnk). Thm* ring(R;in;out) Thm* Thm* Inj(\|R\|; ; uid) Thm* Thm* loc.(ring-leader1(loc;R;uid;out;in)) Thm* realizes es.ldr:\|R\|. Thm* realizes es.e@ldr.kind(e) = locl("leader") Thm* realizes es.& (i:\|R\|. e@i.kind(e) = locl("leader") i = ldr \|R\|)	[ring-leader1__realizes]
Thm* P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = "trigger" Thm* Thm* locl(a) = k Thm* Thm* loc.(trigger1(loc;T;A;P;i;k;a;x)) Thm* realizes es.(vartype(i;x) r A) Thm* realizes es.& e@i.kind(e) = k Knd (valtype(e) r T) Thm* realizes es.& e'@i.kind(e') = locl(a) Thm* realizes es.& e'@i. Thm* realizes es.& (e:E. Thm* realizes es.& ((e <loc e') & kind(e) = k Knd & P((x when e),val(e))) Thm* realizes es.& e@i.kind(e) = k Knd Thm* realizes es.& e@i. Thm* realizes es.& P((x when e),val(e)) e'@i.kind(e') = locl(a) Knd	[trigger1__realizes]
Thm* P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = "trigger" Thm* Thm* locl(a) = k d-feasible(loc.(trigger1(loc;T;A;P;i;k;a;x)))	[trigger1__feasible]
Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = "trigger" locl(a) = k trigger1(loc;T;A;P;i;k;a;x) MsgA List	[trigger1_wf]
Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = "trigger" Thm* Thm* locl(a) = k (A,Btrigger1(loc;T;A;P;i;k;a;x).A \|\|+ B)	[trigger1__compatible]
Thm* a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x Thm* Thm* A Thm* Thm* T Thm* Thm* loc.(send-once(loc;T;A;a;f;tg;l;x)) Thm* realizes es.(vartype(source(l);x) r A) Thm* realizes es.& (e:E. kind(e) = rcv(l; tg) Knd (valtype(e) r T)) Thm* realizes es.& (e:E. Thm* realizes es.& (kind(e) = rcv(l; tg) Knd Thm* realizes es.& (& val(e) = f((x when sender(e))) T Thm* realizes es.& (& & kind(sender(e)) = locl(a) Knd Thm* realizes es.& (& & (e':E. Thm* realizes es.& (& & (kind(e') = rcv(l; tg) Knd Thm* realizes es.& (& & ( Thm* realizes es.& (& & (kind(sender(e')) = locl(a) Knd e' = e E))	[send-once__realizes]
Thm* a,i:Id. Thm* loc.(once(loc;a;i)) Thm* realizes es.e@i.kind(e) = locl(a) Thm* realizes es.& e@i.e'@i.kind(e) = locl(a) Thm* realizes es.& e@i.e'@i. Thm* realizes es.& kind(e') = locl(a) Knd e = e' E	[once__realizes]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:Top. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* ma-single-effect(d1; da; k; x; f) \|\|+ (with ds: ds Thm* maction a:T Thm* mprecondition a(v) is Thm* mP s v)	[ma-single-effect-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* ma-single-sends(d1; da; k; l; f) \|\|+ (with ds: ds Thm* maction a:T Thm* mprecondition a(v) is Thm* mP s v)	[ma-single-sends-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ ma-single-sends(d1; da; k; l; f)	[ma-single-pre-ma-single-sends-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd, Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ ma-single-effect(d1; da; k; x; f)	[ma-single-pre-init-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd, Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ ma-single-sends(d1; da; k; l; f)	[ma-single-pre-init-ma-single-sends-compatible]
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]
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]
Def send-once(loc;T;A;a;f;tg;l;x) Def == [(once(loc;a;source(l))); Def == [if loc = source(l) Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])) Def == [else fi]	[send-once]
Def once(loc;a;i) Def == if loc = i Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x); Def == if [only members of [locl(a)] affect "done" :; Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] Def == else nil fi	[once]