Nuprl - mb_event_system_7 Citations of not

mb event system 7 Sections EventSystems Doc

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

A == A

False

is mentioned by

Thm* R:(Id), in,out:(|R|IdLnk), i,j:|R|.
Thm* ring(R;in;out)  i = p(j)  d(i;p(j)) = d(i;j)-1 [rdist-rprev]

Thm* R:(Id), in,out:(|R|IdLnk), i,j:|R|.
Thm* ring(R;in;out)
Thm*
Thm* x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j) [rdist-property]

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* 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* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  recognizer1(loc;T;A;P;k;i;r;x)  MsgA List [recognizer1_wf]

Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  (A,Brecognizer1(loc;T;A;P;k;i;r;x).A ||+ B) [recognizer1__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: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* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x  A  T  send-once(loc;T;A;a;f;tg;l;x)  MsgA List [send-once_wf]

Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x  A  T  (A,Bsend-once(loc;T;A;a;f;tg;l;x).A ||+ B) [send-once__compatible]

Thm* x:Id, t,v:Top, x1:Id, t1,v1:Top.
Thm* x = x1  x : t initially x = v ||+ x1 : t1 initially x1 = v1 [ma-single-init-ma-single-init-compatible]

Thm* x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type.
Thm* x = x1
Thm*
Thm* only members of L affect x :t ||+ only members of L1 affect x1 :t1 [ma-single-frame-ma-single-frame-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd,
Thm* d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* <k,x> = <k1,x1>
Thm*
Thm* ma-single-effect(ds; da; k; x; f) ||+ ma-single-effect(d1; d2; k1; x1; f1) [ma-single-effect-ma-single-effect-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* <k,l> = <k1,l1>
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-sends(d1; d2; k1; l1; f1) [ma-single-sends-ma-single-sends-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top,
Thm* d1:x:Id fp-> Type, P1:Top.
Thm* ds || d1
Thm*
Thm* a = a1
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ (with ds: d1
Thm* aaction a1:T1
Thm* aprecondition a1(v) is
Thm* aP1 s v) [ma-single-pre-init-ma-single-pre-compatible]

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]

Thm* i,x:Id, k:Knd, T:Type.
Thm* @i: only members of [k] affect x :T  Dsys
Thm* & (D:Dsys.
Thm* & (@i: only members of [k] affect x :T  D
Thm* & (
Thm* & (D
Thm* & (realizes es.(vartype(i;x) r T)
Thm* & (realizes es.& e@i.((x after e) = (x when e)  T  kind(e) = k  Knd)
Thm* & (realizes es.& & (kind(e) = k  Knd  (x after e) = (x when e)  T)) [frame-rule1]

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]

Thm* i:Id, L:Knd List, x:Id, T:Type.
Thm* @i: only members of L affect x :T  Dsys
Thm* & (D:Dsys.
Thm* & (@i: only members of L affect x :T  D
Thm* & (
Thm* & (D
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))) [s-frame-rule]

Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type.
Thm* (rcv(l; tg) = k  T = B)
Thm*
Thm* (f:(ABT), c:(AB).
Thm* (@source(l): ma-single-sends1(A;
Thm* (@source(l): ma-single-sends1(B;
Thm* (@source(l): ma-single-sends1(T;
Thm* (@source(l): ma-single-sends1(x;
Thm* (@source(l): ma-single-sends1(k;
Thm* (@source(l): ma-single-sends1(l;
Thm* (@source(l): ma-single-sends1(tg;
Thm* (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi))
Thm* ( Dsys
Thm* (& (D:Dsys.
Thm* (& (@source(l): ma-single-sends1(A;
Thm* (& (@source(l): ma-single-sends1(B;
Thm* (& (@source(l): ma-single-sends1(T;
Thm* (& (@source(l): ma-single-sends1(x;
Thm* (& (@source(l): ma-single-sends1(k;
Thm* (& (@source(l): ma-single-sends1(l;
Thm* (& (@source(l): ma-single-sends1(tg;
Thm* (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)
Thm* (& (@source(l): ma-single-sends1()  D
Thm* (& (
Thm* (& (D
Thm* (& (realizes es.(vartype(source(l);x) r A)
Thm* (& (realizes es.& (e:E.
Thm* (& (realizes es.& (loc(e) = source(l)  Id
Thm* (& (realizes es.& (
Thm* (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B))
Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T))
Thm* (& (realizes es.& (e:E.
Thm* (& (realizes es.& (loc(e) = source(l)  Id
Thm* (& (realizes es.& (
Thm* (& (realizes es.& (kind(e) = k  Knd
Thm* (& (realizes es.& (
Thm* (& (realizes es.& ((c((x when e),val(e))
Thm* (& (realizes es.& ((
Thm* (& (realizes es.& (((e':E.
Thm* (& (realizes es.& (((kind(e') = rcv(l; tg)  Knd
Thm* (& (realizes es.& (((& sender(e') = e  E
Thm* (& (realizes es.& (((& & (e'':E.
Thm* (& (realizes es.& (((& & (kind(e'') = rcv(l; tg)  Knd
Thm* (& (realizes es.& (((& & (
Thm* (& (realizes es.& (((& & (sender(e'') = e  E  e'' = e'  E)
Thm* (& (realizes es.& (((& & val(e') = f((x when e),val(e))  T))
Thm* (& (realizes es.& (& (c((x when e),val(e))
Thm* (& (realizes es.& (& (
Thm* (& (realizes es.& (& ((e':E.
Thm* (& (realizes es.& (& ((kind(e') = rcv(l; tg)  Knd
Thm* (& (realizes es.& (& ((& sender(e') = e  E))))) [conditional-send1-rule]

Def spanner(f;T;to;from)
Def == (l:Edge(T). f(l) = f(inverse(l)))
Def == & (i:|T|, l1,l2:Edge(T).
Def == & ((l1  to(i))
Def == & (
Def == & ((l2  to(i))  l1 = l2  IdLnk  (f(l1))  (f(l2))) [spanner]

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: core bool 1 int 2 list 1 sqequal 1 rel 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 5 mb event system 6 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), in,out:(\|R\|IdLnk), i,j:\|R\|. Thm* ring(R;in;out) i = p(j) d(i;p(j)) = d(i;j)-1	[rdist-rprev]
Thm* R:(Id), in,out:(\|R\|IdLnk), i,j:\|R\|. Thm* ring(R;in;out) Thm* Thm* x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j) x.n(x)^k(i) = j)	[rdist-property]
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* 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* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A T x = r recognizer1(loc;T;A;P;k;i;r;x) MsgA List	[recognizer1_wf]
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A T x = r (A,Brecognizer1(loc;T;A;P;k;i;r;x).A \|\|+ B)	[recognizer1__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: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* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x A T send-once(loc;T;A;a;f;tg;l;x) MsgA List	[send-once_wf]
Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x A T (A,Bsend-once(loc;T;A;a;f;tg;l;x).A \|\|+ B)	[send-once__compatible]
Thm* x:Id, t,v:Top, x1:Id, t1,v1:Top. Thm* x = x1 x : t initially x = v \|\|+ x1 : t1 initially x1 = v1	[ma-single-init-ma-single-init-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type. Thm* x = x1 Thm* Thm* only members of L affect x :t \|\|+ only members of L1 affect x1 :t1	[ma-single-frame-ma-single-frame-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd, Thm* d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* <k,x> = <k1,x1> Thm* Thm* ma-single-effect(ds; da; k; x; f) \|\|+ ma-single-effect(d1; d2; k1; x1; f1)	[ma-single-effect-ma-single-effect-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* <k,l> = <k1,l1> Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ ma-single-sends(d1; d2; k1; l1; f1)	[ma-single-sends-ma-single-sends-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top, Thm* d1:x:Id fp-> Type, P1:Top. Thm* ds \|\| d1 Thm* Thm* a = a1 Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ (with ds: d1 Thm* aaction a1:T1 Thm* aprecondition a1(v) is Thm* aP1 s v)	[ma-single-pre-init-ma-single-pre-compatible]
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]
Thm* i,x:Id, k:Knd, T:Type. Thm* @i: only members of [k] affect x :T Dsys Thm* & (D:Dsys. Thm* & (@i: only members of [k] affect x :T D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& e@i.((x after e) = (x when e) T kind(e) = k Knd) Thm* & (realizes es.& & (kind(e) = k Knd (x after e) = (x when e) T))	[frame-rule1]
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]
Thm* i:Id, L:Knd List, x:Id, T:Type. Thm* @i: only members of L affect x :T Dsys Thm* & (D:Dsys. Thm* & (@i: only members of L affect x :T D Thm* & ( Thm* & (D 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)))	[s-frame-rule]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k T = B) Thm* Thm* (f:(ABT), c:(AB). Thm* (@source(l): ma-single-sends1(A; Thm* (@source(l): ma-single-sends1(B; Thm* (@source(l): ma-single-sends1(T; Thm* (@source(l): ma-single-sends1(x; Thm* (@source(l): ma-single-sends1(k; Thm* (@source(l): ma-single-sends1(l; Thm* (@source(l): ma-single-sends1(tg; Thm* (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)) Thm* ( Dsys Thm* (& (D:Dsys. Thm* (& (@source(l): ma-single-sends1(A; Thm* (& (@source(l): ma-single-sends1(B; Thm* (& (@source(l): ma-single-sends1(T; Thm* (& (@source(l): ma-single-sends1(x; Thm* (& (@source(l): ma-single-sends1(k; Thm* (& (@source(l): ma-single-sends1(l; Thm* (& (@source(l): ma-single-sends1(tg; Thm* (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi) Thm* (& (@source(l): ma-single-sends1() D Thm* (& ( Thm* (& (D Thm* (& (realizes es.(vartype(source(l);x) r A) Thm* (& (realizes es.& (e:E. Thm* (& (realizes es.& (loc(e) = source(l) Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k Knd (valtype(e) r B)) Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg) Knd (valtype(e) r T)) Thm* (& (realizes es.& (e:E. Thm* (& (realizes es.& (loc(e) = source(l) Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k Knd Thm* (& (realizes es.& ( Thm* (& (realizes es.& ((c((x when e),val(e)) Thm* (& (realizes es.& (( Thm* (& (realizes es.& (((e':E. Thm* (& (realizes es.& (((kind(e') = rcv(l; tg) Knd Thm* (& (realizes es.& (((& sender(e') = e E Thm* (& (realizes es.& (((& & (e'':E. Thm* (& (realizes es.& (((& & (kind(e'') = rcv(l; tg) Knd Thm* (& (realizes es.& (((& & ( Thm* (& (realizes es.& (((& & (sender(e'') = e E e'' = e' E) Thm* (& (realizes es.& (((& & val(e') = f((x when e),val(e)) T)) Thm* (& (realizes es.& (& (c((x when e),val(e)) Thm* (& (realizes es.& (& ( Thm* (& (realizes es.& (& ((e':E. Thm* (& (realizes es.& (& ((kind(e') = rcv(l; tg) Knd Thm* (& (realizes es.& (& ((& sender(e') = e E)))))	[conditional-send1-rule]
Def spanner(f;T;to;from) Def == (l:Edge(T). f(l) = f(inverse(l))) Def == & (i:\|T\|, l1,l2:Edge(T). Def == & ((l1 to(i)) Def == & ( Def == & ((l2 to(i)) l1 = l2 IdLnk (f(l1)) (f(l2)))	[spanner]
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]