Nuprl - mb_event_system_7 Citations of ma-join-list

mb event system 7 Sections EventSystems Doc

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

(L) == reduce(

A,B. A

B;;L)

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* R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|; ; uid)  d-feasible(loc.(ring-leader1(loc;R;uid;out;in))) [ring-leader1__feasible]

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* P:(AT), k:Knd, i,r,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = r
Thm*
Thm* loc.(recognizer1(loc;T;A;P;k;i;r;x))
Thm* realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T)
Thm* realizes es.& (vartype(i;x) r A)
Thm* realizes es.& e@i.first(e)  (r when e) = false
Thm* realizes es.& e'@i.(r after e')
Thm* realizes es.& e'@i.
Thm* realizes es.& e'@i.(e:E.
Thm* realizes es.& e'@i.((e <loc e')  e = e'  E
Thm* realizes es.& e'@i.(& kind(e) = k  Knd
Thm* realizes es.& e'@i.(& P((x when e),val(e))) [recognizer1__realizes]

Thm* P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  d-feasible(loc.(recognizer1(loc;T;A;P;k;i;r;x))) [recognizer1__feasible]

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:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x  A  T  d-feasible(loc.(send-once(loc;T;A;a;f;tg;l;x))) [send-once__feasible]

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,i:Id. d-feasible(loc.(once(loc;a;i))) [once__feasible]

Thm* c:T, x,i:Id.
Thm* loc.(Dconstant(loc;T;c;x;i))
Thm* realizes es.e@i.(x when e) = c  T [Dconstant__realizes]

Thm* c:T, x,i:Id. d-feasible(loc.(Dconstant(loc;T;c;x;i))) [Dconstant__feasible]

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 trigger1(loc;T;A;P;i;k;a;x)
Def == [(recognizer1(loc;T;A;P;k;i;"trigger";x));
Def == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else  fi] [trigger1]

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]

In prior sections: mb event system 6

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* R:(Id), uid:(\|R\|), out,in:(\|R\|IdLnk). Thm* ring(R;in;out) Thm* Thm* Inj(\|R\|; ; uid) d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))	[ring-leader1__feasible]
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* P:(AT), k:Knd, i,r,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = r Thm* Thm* loc.(recognizer1(loc;T;A;P;k;i;r;x)) Thm* realizes es.e@i.kind(e) = k Knd (valtype(e) r T) Thm* realizes es.& (vartype(i;x) r A) Thm* realizes es.& e@i.first(e) (r when e) = false Thm* realizes es.& e'@i.(r after e') Thm* realizes es.& e'@i. Thm* realizes es.& e'@i.(e:E. Thm* realizes es.& e'@i.((e <loc e') e = e' E Thm* realizes es.& e'@i.(& kind(e) = k Knd Thm* realizes es.& e'@i.(& P((x when e),val(e)))	[recognizer1__realizes]
Thm* P:(AT), k:Knd, i,r,x:Id. Thm* A T x = r d-feasible(loc.(recognizer1(loc;T;A;P;k;i;r;x)))	[recognizer1__feasible]
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:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x A T d-feasible(loc.(send-once(loc;T;A;a;f;tg;l;x)))	[send-once__feasible]
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,i:Id. d-feasible(loc.(once(loc;a;i)))	[once__feasible]
Thm* c:T, x,i:Id. Thm* loc.(Dconstant(loc;T;c;x;i)) Thm* realizes es.e@i.(x when e) = c T	[Dconstant__realizes]
Thm* c:T, x,i:Id. d-feasible(loc.(Dconstant(loc;T;c;x;i)))	[Dconstant__feasible]
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 trigger1(loc;T;A;P;i;k;a;x) Def == [(recognizer1(loc;T;A;P;k;i;"trigger";x)); Def == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else fi]	[trigger1]
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]