Def P  Q == PQ

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)), 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* 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), 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* 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* 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* 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* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t || x1 : t1 Thm*  Thm* x1 : t1 initially x1 = v ||+ only members of L affect x :t	[ma-single-init-ma-single-frame-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t || x1 : t1 Thm*  Thm* only members of L affect x :t ||+ x1 : t1 initially x1 = v	[ma-single-frame-ma-single-init-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, Thm* v:t. Thm* ds || x1 : t Thm*  Thm* x1 : t initially x1 = v ||+ ma-single-effect(ds; da; k; x; f)	[ma-single-init-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, Thm* v:t. Thm* ds || x1 : t Thm*  Thm* ma-single-effect(ds; da; k; x; f) ||+ x1 : t initially x1 = v	[ma-single-effect-ma-single-init-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds || x1 : t Thm*  Thm* (x = x1  (k  L)) Thm*  Thm* only members of L affect x1 :t ||+ ma-single-effect(ds; da; k; x; f)	[ma-single-frame-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds || x1 : t Thm*  Thm* (x = x1  (k  L)) Thm*  Thm* ma-single-effect(ds; da; k; x; f) ||+ only members of L affect x1 :t	[ma-single-effect-ma-single-frame-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, t:Type, v:t. Thm* ds || x : t  x : t initially x = v ||+ ma-single-sends(ds; da; k; l; f)	[ma-single-init-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, t:Type, v:t. Thm* ds || x : t  ma-single-sends(ds; da; k; l; f) ||+ x : t initially x = v	[ma-single-sends-ma-single-init-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* only members of L affect x :t ||+ ma-single-sends(ds; da; k; l; f)	[ma-single-frame-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* ma-single-sends(ds; da; k; l; f) ||+ only members of L affect x :t	[ma-single-sends-ma-single-frame-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* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds || d1 Thm*  Thm* da || d2 Thm*  Thm* ma-single-effect(d1; d2; k1; x; f1) ||+ ma-single-sends(ds; da; k; l; f)	[ma-single-effect-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds || d1 Thm*  Thm* da || d2 Thm*  Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-effect(d1; d2; k1; x; f1)	[ma-single-sends-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. Thm* ds || x : t Thm*  Thm* x : t initially x = v ||+ (with ds: ds Thm* xaction a:T Thm* xprecondition a(v) is Thm* xP s v)	[ma-single-init-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. Thm* ds || x : t Thm*  Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) ||+ x : t initially x = v	[ma-single-pre-ma-single-init-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* only members of L affect x :t ||+ (with ds: ds Thm* oaction a:T Thm* oprecondition a(v) is Thm* oP s v)	[ma-single-frame-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) ||+ only members of L affect x :t	[ma-single-pre-ma-single-frame-compatible]
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:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id, Thm* t:Type, v:t. Thm* ds || x : t Thm*  Thm* (x  dom(init)  init(x) = v  t) Thm*  Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) ||+ x : t initially x = v	[ma-single-pre-init-ma-single-init-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, Thm* L:Knd List, t:Type. Thm* ds || x : t Thm*  Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) ||+ only members of L affect x :t	[ma-single-pre-init-ma-single-frame-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* 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* 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]
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,x:Id, T:Type. Thm* @i: only members of nil affect x :T  Dsys Thm* & (D:Dsys.  Thm* & (@i: only members of nil affect x :T  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r T) & e@i.(x after e) = (x when e)  T)	[frame-rule0]
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* i:Id, T:Type, v:T, x:Id. Thm* @i: x : T initially x = v  Dsys Thm* & (D:Dsys.  Thm* & (@i: x : T initially x = v  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T))	[s-init-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]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* (f:(ABT).  Thm* (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))])) Thm* ( Dsys Thm* (& (D:Dsys.  Thm* (& (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]) 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.& ((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))))	[s-unconditional-send1-rule]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)). Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  Dsys Thm* & (D:Dsys.  Thm* & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  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.& ((L:{e':E| kind(e') = rcv(l; tg)  Knd } List.  Thm* & (realizes es.& (((e':E.  Thm* & (realizes es.& ((((e'  L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e))  T List)))	[s-sends-rule1]
Def spanner-root(f;T;to;from;i) == l:Edge(T). (l  to(i))  (f(l))	[spanner-root]
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 bi-tree(T;to;from) Def == bi-graph(T;to;from) Def == & (i,j:|T|. Def == & (p:Edge(T) List.  Def == & (lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)) Def == & (L:|T| List. i:|T|. (i  L)) Def == & |T|	[bi-tree]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 union rel 1 mb basic 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 4 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