Nuprl - mb_event_system_5 Citations of Knd

mb event system 5 Sections EventSystems Doc

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

Id)+Id

is mentioned by

Thm* M1,M2:MsgA.
Thm* M1  M2
Thm*
Thm* (k:Knd, l:IdLnk, tg:Id.
Thm* (M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>)) [ma-sframe-sub]

Thm* M1,M2:MsgA.
Thm* M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x)) [ma-frame-sub]

Thm* M1,M2:MsgA.
Thm* M1  M2
Thm*
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg))
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List.
Thm* (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i)) [ma-send-sub]

Thm* M1,M2:MsgA.
Thm* M1  M2
Thm*
Thm* (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
Thm* (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w)) [ma-ef-sub]

Thm* M1,M2:MsgA, k:Knd. M1  M2  (M2.da(k) r M1.da(k)) [ma-da-sub]

Thm* x,y:Id, k:Knd, A,B,T:Type, f:(ABTA).
Thm* y = x  ma-single-effect1(x;A;y;B;k;T;f)  MsgA [ma-single-effect1_wf]

Thm* x:Id, k:Knd, A,T:Type, f:(ATA). ma-single-effect0(x;A;k;T;f)  MsgA [ma-single-effect0_wf]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void).
Thm* ma-single-effect(ds; da; k; x; f)  MsgA [ma-single-effect_wf]

Thm* l:IdLnk, tg:Id, L:Knd List. only L sends on (l with tg)  MsgA [ma-single-sframe_wf]

Thm* x:Id, L:Knd List, t:Type. only members of L affect x :t  MsgA [ma-single-frame_wf]

Thm* M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>)  Prop [ma-sframe_wf]

Thm* M:MsgA, k:Knd, x:Id. M.frame(k affects x)  Prop [ma-frame_wf]

Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg))
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List.
Thm* M.send(k;l;s;v;ms;i)  Prop [ma-send_wf]

Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x).
Thm* M.ef(k,x,s,v,w)  Prop [ma-ef_wf]

Thm* M:MsgA, k:Knd. M.V(k)  Type [ma-v_wf]

Thm* M:MsgA, a:Knd. M.da(a)  Type [ma-da_wf]

Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type.
Thm* (ltg  da-outlinks(da1  da2;i))
Thm*
Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i)) [da-outlinks-join]

Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type.
Thm* (ltg  da-outlinks(k : T;i))
Thm*
Thm* isrcv(k) & source(lnk(k)) = i
Thm* & (1of(ltg) ~ lnk(k))
Thm* & (1of(2of(ltg)) ~ tag(k))
Thm* & 2of(2of(ltg)) = T [da-outlinks-single]

Thm* da:k:Knd fp-> Type, i:Id. da-outlinks(da;i)  (IdLnkIdType) List [da-outlinks_wf]

Thm* da:k:Knd fp-> Type, k:{k:Knd| k  dom(da) & isrcv(k) }.
Thm* da-outlink-f(da;k)  IdLnkIdType [da-outlink-f_wf]

Def PossibleWorld(D;w)
Def == FairFifo
Def == & (i,x:Id. vartype(i;x) r M(i).ds(x))
Def == & & (i:Id, a:Action(i).
Def == & & (isnull(a)  (valtype(i;a) r M(i).da(kind(a))))
Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg)))
Def == & & (i,x:Id. M(i).init(x,s(i;0).x))
Def == & & (i:Id, t:.
Def == & & (isnull(a(i;t))
Def == & & (
Def == & & ((islocal(kind(a(i;t)))
Def == & & ((
Def == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
Def == & & (& (x:Id.
Def == & & (& (M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
Def == & & (& (l:IdLnk.
Def == & & (& (M(i).send(kind(a(i;t));l;x.
Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
Def == & & (& (x:Id.
Def == & & (& (M(i).frame(kind(a(i;t)) affects x)
Def == & & (& (
Def == & & (& (s(i;t).x = s(i;t+1).x  M(i).ds(x))
Def == & & (& (l:IdLnk, tg:Id.
Def == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>)
Def == & & (& (
Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List))
Def == & & (i,a:Id, t:.
Def == & & (t':.
Def == & & (tt'
Def == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a)
Def == & & (&  a declared in M(i)
Def == & & (&  unsolvable M(i).pre(a,x.s(i;t').x)) [possible-world]

In prior sections: mb event system 1 mb event system 2 mb event system 3 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 5 Sections EventSystems Doc

Thm* M1,M2:MsgA. Thm* M1 M2 Thm* Thm* (k:Knd, l:IdLnk, tg:Id. Thm* (M2.sframe(k sends <l,tg>) M1.sframe(k sends <l,tg>))	[ma-sframe-sub]
Thm* M1,M2:MsgA. Thm* M1 M2 (k:Knd, x:Id. M2.frame(k affects x) M1.frame(k affects x))	[ma-frame-sub]
Thm* M1,M2:MsgA. Thm* M1 M2 Thm* Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg)) Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List. Thm* (M2.send(k;l;s;v;ms;i) M1.send(k;l;s;v;ms;i))	[ma-send-sub]
Thm* M1,M2:MsgA. Thm* M1 M2 Thm* Thm* (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x). Thm* (M2.ef(k,x,s,v,w) M1.ef(k,x,s,v,w))	[ma-ef-sub]
Thm* M1,M2:MsgA, k:Knd. M1 M2 (M2.da(k) r M1.da(k))	[ma-da-sub]
Thm* x,y:Id, k:Knd, A,B,T:Type, f:(ABTA). Thm* y = x ma-single-effect1(x;A;y;B;k;T;f) MsgA	[ma-single-effect1_wf]
Thm* x:Id, k:Knd, A,T:Type, f:(ATA). ma-single-effect0(x;A;k;T;f) MsgA	[ma-single-effect0_wf]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* ma-single-effect(ds; da; k; x; f) MsgA	[ma-single-effect_wf]
Thm* l:IdLnk, tg:Id, L:Knd List. only L sends on (l with tg) MsgA	[ma-single-sframe_wf]
Thm* x:Id, L:Knd List, t:Type. only members of L affect x :t MsgA	[ma-single-frame_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>) Prop	[ma-sframe_wf]
Thm* M:MsgA, k:Knd, x:Id. M.frame(k affects x) Prop	[ma-frame_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg)) Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List. Thm* M.send(k;l;s;v;ms;i) Prop	[ma-send_wf]
Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). Thm* M.ef(k,x,s,v,w) Prop	[ma-ef_wf]
Thm* M:MsgA, k:Knd. M.V(k) Type	[ma-v_wf]
Thm* M:MsgA, a:Knd. M.da(a) Type	[ma-da_wf]
Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg da-outlinks(da1 da2;i)) Thm* Thm* (ltg da-outlinks(da1;i)) (ltg da-outlinks(da2;i))	[da-outlinks-join]
Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg da-outlinks(k : T;i)) Thm* Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]
Thm* da:k:Knd fp-> Type, i:Id. da-outlinks(da;i) (IdLnkIdType) List	[da-outlinks_wf]
Thm* da:k:Knd fp-> Type, k:{k:Knd\| k dom(da) & isrcv(k) }. Thm* da-outlink-f(da;k) IdLnkIdType	[da-outlink-f_wf]
Def PossibleWorld(D;w) Def == FairFifo Def == & (i,x:Id. vartype(i;x) r M(i).ds(x)) Def == & & (i:Id, a:Action(i). Def == & & (isnull(a) (valtype(i;a) r M(i).da(kind(a)))) Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))) Def == & & (i,x:Id. M(i).init(x,s(i;0).x)) Def == & & (i:Id, t:. Def == & & (isnull(a(i;t)) Def == & & ( Def == & & ((islocal(kind(a(i;t))) Def == & & (( Def == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) Def == & & (& (x:Id. Def == & & (& (M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)) Def == & & (& (l:IdLnk. Def == & & (& (M(i).send(kind(a(i;t));l;x. Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)) Def == & & (& (x:Id. Def == & & (& (M(i).frame(kind(a(i;t)) affects x) Def == & & (& ( Def == & & (& (s(i;t).x = s(i;t+1).x M(i).ds(x)) Def == & & (& (l:IdLnk, tg:Id. Def == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>) Def == & & (& ( Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil Msg List)) Def == & & (i,a:Id, t:. Def == & & (t':. Def == & & (tt' Def == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a) Def == & & (& a declared in M(i) Def == & & (& unsolvable M(i).pre(a,x.s(i;t').x))	[possible-world]