Nuprl - mb_event_system_7 Citations of bool

mb event system 7 Sections EventSystems Doc

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

== Unit+Unit

is mentioned by

Thm* T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)).
Thm* bi-tree(T;to;from)
Thm*
Thm* spanner(f;T;to;from)
Thm*
Thm* (i,j:|T|.
Thm* (spanner-root(f;T;to;from;i)  spanner-root(f;T;to;from;j)  i = j) [spanner-root-unique]

Thm* T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)).
Thm* bi-tree(T;to;from)
Thm*
Thm* spanner(f;T;to;from)  (i:|T|. spanner-root(f;T;to;from;i)) [spanner-root-exists]

Thm* T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)).
Thm* bi-graph(T;to;from)  spanner(f;T;to;from)  Prop [spanner_wf]

Thm* T:(Id), to,from:(|T|(IdLnk List)).
Thm* bi-tree(T;to;from)  (n:. p:Edge(T) List. lpath(p)  ||p||n) [bi-tree-diameter]

Thm* G:(Id), to,from:(|G|(IdLnk List)). bi-tree(G;to;from)  Prop [bi-tree_wf]

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)  ((inverse(e)  from(i))  destination(e) = i) [edge-inv-from]

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)  ((inverse(e)  to(i))  source(e) = i) [edge-inv-to]

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)  ((e  from(i))  source(e) = i) [edge-from]

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)  ((e  to(i))  destination(e) = i) [edge-to]

Thm* G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G).
Thm* bi-graph(G;to;from)  inverse(l)  Edge(G) [bi-graph-inv_wf]

Thm* G:(Id), to,from:(|G|(IdLnk List)), i:|G|.
Thm* bi-graph(G;to;from)  from(i)  Edge(G) List [bi-graph-from_wf]

Thm* G:(Id), to,from:(|G|(IdLnk List)), i:|G|.
Thm* bi-graph(G;to;from)  to(i)  Edge(G) List [bi-graph-to_wf]

Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)  destination(u)  |T| [dst-edge]

Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)  source(u)  |T| [src-edge]

Thm* G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G).
Thm* bi-graph(G;to;from)  lnk-inv(l)  Edge(G) [inv-is-edge]

Thm* G:(Id), to,from:(|G|(IdLnk List)). bi-graph(G;to;from)  Prop [bi-graph_wf]

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

Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|; ; uid)  (A,Bring-leader1(loc;R;uid;out;in).A ||+ B) [ring-leader1__compatible]

Thm* R:(Id), x,y:|R|. Dec(x = y) [decidable__rset_equal]

Thm* R:(Id). SQType(|R|) [rset_sq]

Thm* R:(Id), in,out:(|R|IdLnk).
Thm* ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L))) [ring-list]

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).
Thm* ring(R;in;out)  (i,j:|R|. n(i) = n(j)  i = j) [rnext-one-one]

Thm* R:(Id), in,out:(|R|IdLnk), j:|R|. ring(R;in;out)  n(p(j)) = j [rnext-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* R:(Id), in,out:(|R|IdLnk), i,j:|R|. ring(R;in;out)  d(i;j)   [rdist_wf]

Thm* R:(Id), in,out:(|R|IdLnk), i:|R|. ring(R;in;out)  p(i)  |R| [rprev_wf]

Thm* R:(Id), in,out:(|R|IdLnk), i:|R|. ring(R;in;out)  n(i)  |R| [rnext_wf]

Thm* R:(Id), in,out:(|R|IdLnk). ring(R;in;out)  Prop [ring_wf]

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* 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 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 recognizer1(loc;T;A;P;k;i;r;x)
Def == if loc = i
Def == if [r :  initially r = false;
Def == if [only members of [k] affect r :;
Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)]
Def == else nil fi [recognizer1]

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: bool 1 list 1 sqequal 1 rel 1 mb nat mb list 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 5 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* T:(Id), to,from:(\|T\|(IdLnk List)), f:(Edge(T)). Thm* bi-tree(T;to;from) Thm* Thm* spanner(f;T;to;from) Thm* Thm* (i,j:\|T\|. Thm* (spanner-root(f;T;to;from;i) spanner-root(f;T;to;from;j) i = j)	[spanner-root-unique]
Thm* T:(Id), to,from:(\|T\|(IdLnk List)), f:(Edge(T)). Thm* bi-tree(T;to;from) Thm* Thm* spanner(f;T;to;from) (i:\|T\|. spanner-root(f;T;to;from;i))	[spanner-root-exists]
Thm* T:(Id), to,from:(\|T\|(IdLnk List)), f:(Edge(T)). Thm* bi-graph(T;to;from) spanner(f;T;to;from) Prop	[spanner_wf]
Thm* T:(Id), to,from:(\|T\|(IdLnk List)). Thm* bi-tree(T;to;from) (n:. p:Edge(T) List. lpath(p) \|\|p\|\|n)	[bi-tree-diameter]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)). bi-tree(G;to;from) Prop	[bi-tree_wf]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), e:Edge(G), i:\|G\|. Thm* bi-graph(G;to;from) ((inverse(e) from(i)) destination(e) = i)	[edge-inv-from]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), e:Edge(G), i:\|G\|. Thm* bi-graph(G;to;from) ((inverse(e) to(i)) source(e) = i)	[edge-inv-to]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), e:Edge(G), i:\|G\|. Thm* bi-graph(G;to;from) ((e from(i)) source(e) = i)	[edge-from]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), e:Edge(G), i:\|G\|. Thm* bi-graph(G;to;from) ((e to(i)) destination(e) = i)	[edge-to]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), l:Edge(G). Thm* bi-graph(G;to;from) inverse(l) Edge(G)	[bi-graph-inv_wf]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), i:\|G\|. Thm* bi-graph(G;to;from) from(i) Edge(G) List	[bi-graph-from_wf]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), i:\|G\|. Thm* bi-graph(G;to;from) to(i) Edge(G) List	[bi-graph-to_wf]
Thm* T:(Id), to,from:(\|T\|(IdLnk List)), u:Edge(T). Thm* bi-graph(T;to;from) destination(u) \|T\|	[dst-edge]
Thm* T:(Id), to,from:(\|T\|(IdLnk List)), u:Edge(T). Thm* bi-graph(T;to;from) source(u) \|T\|	[src-edge]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)), l:Edge(G). Thm* bi-graph(G;to;from) lnk-inv(l) Edge(G)	[inv-is-edge]
Thm* G:(Id), to,from:(\|G\|(IdLnk List)). bi-graph(G;to;from) Prop	[bi-graph_wf]
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* loc:Id, R:(Id), uid:(\|R\|), out,in:(\|R\|IdLnk). Thm* ring(R;in;out) Thm* Thm* Inj(\|R\|; ; uid) ring-leader1(loc;R;uid;out;in) MsgA List	[ring-leader1_wf]
Thm* loc:Id, R:(Id), uid:(\|R\|), out,in:(\|R\|IdLnk). Thm* ring(R;in;out) Thm* Thm* Inj(\|R\|; ; uid) (A,Bring-leader1(loc;R;uid;out;in).A \|\|+ B)	[ring-leader1__compatible]
Thm* R:(Id), x,y:\|R\|. Dec(x = y)	[decidable__rset_equal]
Thm* R:(Id). SQType(\|R\|)	[rset_sq]
Thm* R:(Id), in,out:(\|R\|IdLnk). Thm* ring(R;in;out) (L:\|R\| List. 0<\|\|L\|\| & (i:\|R\|. (i L)))	[ring-list]
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). Thm* ring(R;in;out) (i,j:\|R\|. n(i) = n(j) i = j)	[rnext-one-one]
Thm* R:(Id), in,out:(\|R\|IdLnk), j:\|R\|. ring(R;in;out) n(p(j)) = j	[rnext-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* R:(Id), in,out:(\|R\|IdLnk), i,j:\|R\|. ring(R;in;out) d(i;j)	[rdist_wf]
Thm* R:(Id), in,out:(\|R\|IdLnk), i:\|R\|. ring(R;in;out) p(i) \|R\|	[rprev_wf]
Thm* R:(Id), in,out:(\|R\|IdLnk), i:\|R\|. ring(R;in;out) n(i) \|R\|	[rnext_wf]
Thm* R:(Id), in,out:(\|R\|IdLnk). ring(R;in;out) Prop	[ring_wf]
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* 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 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 recognizer1(loc;T;A;P;k;i;r;x) Def == if loc = i Def == if [r : initially r = false; Def == if [only members of [k] affect r :; Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v) r)] Def == else nil fi	[recognizer1]
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]