Nuprl - mb_event_system_7 Citations of m-sys-at

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def @i: A(j) == if j = i

A else fi

is mentioned by

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]

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