Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
d-subDef D1  D2 == i:Id. M(i M(i)
dsysDef Dsys == IdMsgA
Thm* Dsys  Type{i'}
ma-join-listDef (L) == reduce(A,BA  B;;L)
possible-worldDef PossibleWorld(D;w)
Def == FairFifo
Def == & (i,x:Id. vartype(i;xr M(i).ds(x))
Def == & & (i:Id, a:Action(i).
Def == & & (isnull(a (valtype(i;ar M(i).da(kind(a))))
Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(ltg)))
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))
worldDef World
Def == T:IdIdType
Def == TA:IdIdType
Def == M:IdLnkIdType
Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i)))
Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
Thm* World  Type{i'}
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
alle-atDef e@i.P(e) == e:E. loc(e) = i  Id  P(e)
fair-fifoDef FairFifo
Def == (i:Id, t:l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List)
Def == & (i:Id, t:.
Def == & (isnull(a(i;t))
Def == & (
Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x))
Def == & (& m(i;t) = nil  Msg List)
Def == & (i:Id, t:l:IdLnk.
Def == & (isrcv(l;a(i;t))
Def == & (
Def == & (destination(l) = i
Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg)
Def == & (l:IdLnk, t:.
Def == & (t':
Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
w-esDef ES(the_w;p)
Def == <E
Def == ,product-deq(Id;;IdDeq;NatDeq)
Def == ,(i,x. vartype(i;x))
Def == ,(i,a. V(i;locl(a)))
Def == ,the_w.M
Def == ,
Def == ,(e.loc(e))
Def == ,(e.kind(e))
Def == ,(e.val(e))
Def == ,(x,e. (x when e))
Def == ,(x,e. (x after e))
Def == ,(l,e. sends(l;e))
Def == ,(e.sender(e))
Def == ,(e.index(e))
Def == ,(e.first(e))
Def == ,(e.pred(e))
Def == ,(e,e'e <c e')
Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p)
Def == ,>
IdDef Id == Atom
Thm* Id  Type
recognizer1Def 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,vP(x,v r)]
Def == else nil fi
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
assertDef b == if b True else False fi
Thm* b:b  Prop
es-firstDef first(e)
Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
Def == 1of(es)))))))))))))))
Def == (e)
es-vartypeDef vartype(i;x) == 1of(2of(2of(es)))(i,x)
es-whenDef (x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e)
notDef A == A  False
Thm* A:Prop. (A Prop

About:
pairproductproductlistconsnilboolbfalseifthenelseassertit
natural_numberaddatomunionsetlambdaapplyfunctionuniverseequalmember
topsubtype_relpropimpliesandorfalsetrueallexists
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 7 Sections EventSystems Doc