Nuprl - mb_event_system_7 Citations of l

mb event system 7 Sections EventSystems Doc

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

l) ==

. i<||l|| & x = l[i]

is mentioned by

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

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-> 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* 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: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, 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]

Def Edge(G) == {l:IdLnk| i:|G|. (l  from(i)) } [bi-graph-edge]

Def bi-graph(G;to;from)
Def == i:|G|.
Def == (lto(i).destination(l) = i
Def == & (G(source(l)))
Def == & (l  from(source(l)))
Def == & (lnk-inv(l)  from(i)))
Def == & (lfrom(i).source(l) = i
Def == & & (G(destination(l)))
Def == & & (l  to(destination(l)))
Def == & & (lnk-inv(l)  to(i))) [bi-graph]

In prior sections: mb list 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

mb event system 7 Sections EventSystems Doc

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* R:(Id), in,out:(\|R\|IdLnk). Thm* ring(R;in;out) (L:\|R\| List. 0<\|\|L\|\| & (i:\|R\|. (i L)))	[ring-list]
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-> 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* 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: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, 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]
Def Edge(G) == {l:IdLnk\| i:\|G\|. (l from(i)) }	[bi-graph-edge]
Def bi-graph(G;to;from) Def == i:\|G\|. Def == (lto(i).destination(l) = i Def == & (G(source(l))) Def == & (l from(source(l))) Def == & (lnk-inv(l) from(i))) Def == & (lfrom(i).source(l) = i Def == & & (G(destination(l))) Def == & & (l to(destination(l))) Def == & & (lnk-inv(l) to(i)))	[bi-graph]