mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)

is mentioned by

Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(dak)(da(rcv(ltg))?Void List)) List.
Thm* source(l) = i
Thm* 
Thm* @i: ma-single-sends(dsdaklf Dsys
Thm* & (D:Dsys. 
Thm* & (@i: ma-single-sends(dsdaklf D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& ((valtype(er ma-valtype(da; kind(e))))
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (isrcv(e)
Thm* & (realizes es.& (
Thm* & (realizes es.& (lnk(e) = l  IdLnk
Thm* & (realizes es.& (
Thm* & (realizes es.& ((valtype(er ma-valtype(da; kind(e))))
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = k  Knd
Thm* & (realizes es.& (
Thm* & (realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
Thm* & (realizes es.& (((e':E. 
Thm* & (realizes es.& ((((e'  L)
Thm* & (realizes es.& (((
Thm* & (realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
Thm* & (realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
Thm* & (realizes es.& ((& =
Thm* & (realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
Thm* & (realizes es.& ((&  (tg:Idma-valtype(da; rcv(ltg))) List)))
[s-sends-rule]
Thm* i,x:Id, k:Knd, ds:a:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(State(ds)ma-valtype(dak)ds(x)?Void).
Thm* @i: ma-single-effect(dsdakxf Dsys
Thm* & (D:Dsys. 
Thm* & (@i: ma-single-effect(dsdakxf D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& ((valtype(er ma-valtype(da; kind(e))))
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = k  Knd
Thm* & (realizes es.& (
Thm* & (realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top))
[s-effect-rule]
Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp).
Thm* @i: (with ds: ds action a:T precondition a(v) is P s v)  Dsys
Thm* & (D:Dsys. 
Thm* & (@i: (with ds: ds
Thm* & (@action a:T
Thm* & (@precondition a(v) is
Thm* & (@P s v)  D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = locl(a Knd  (valtype(eT))
Thm* & (realizes es.& (e:E. 
Thm* & (realizes es.& (loc(e) = i  Id
Thm* & (realizes es.& (
Thm* & (realizes es.& ((kind(e) = locl(a Knd  P((z.(z when e)),val(e)))
Thm* & (realizes es.& (& (e':E. 
Thm* & (realizes es.& (& ((e <loc e' e = e'  E
Thm* & (realizes es.& (& (& kind(e') = locl(a Knd
Thm* & (realizes es.& (& (&  (v:TP((z.(z after e')),v)))))
[s-pre-rule]
Thm* i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp),
Thm* init:x:Id fp-> ds(x)?Void.
Thm* (x:Id. x  dom(ds x  dom(init))
Thm* 
Thm* @i: (with ds: ds init: initaction a:T precondition a(v) is P Dsys
Thm* & (D:Dsys. 
Thm* & (@i: (with ds: ds
Thm* & (@init: init
Thm* & (action a:T
Thm* & (aprecondition a(v) is
Thm* & (aP D
Thm* & (
Thm* & (D 
Thm* & (realizes es.(v:TP((x.init(x)?),v))  (e:E. loc(e) = i  Id))
[s-pre-init-rule]
Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp),
Thm* init:x:Id fp-> ds(x)?Void.
Thm* (x:Id. x  dom(ds x  dom(init))
Thm* 
Thm* @i (with ds: ds
Thm* @i init: init
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v) 
Thm* realizes es.(v:TP((x.init(x)?),v))  (e:E. loc(e) = i  Id)
[pre-init-rule]
Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
Thm* @i (with ds: ds
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v) 
Thm* realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = locl(a Knd  (valtype(eT))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id
Thm* realizes es.& (
Thm* realizes es.& ((kind(e) = locl(a Knd  P((z.(z when e)),val(e)))
Thm* realizes es.& (& (e':E. 
Thm* realizes es.& (& ((e <loc e' e = e'  E
Thm* realizes es.& (& (& kind(e') = locl(a Knd
Thm* realizes es.& (& (&  (v:TP((z.(z after e')),v))))
[pre-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(dak)(da(rcv(ltg))?Void List)) List.
Thm* source(l) = i
Thm* 
Thm* d-single-sends(idsdaklf
Thm* realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id  (valtype(er ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (isrcv(e)
Thm* realizes es.& (
Thm* realizes es.& (lnk(e) = l  IdLnk
Thm* realizes es.& (
Thm* realizes es.& ((valtype(er ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = k  Knd
Thm* realizes es.& (
Thm* realizes es.& ((L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List. 
Thm* realizes es.& (((e':E. 
Thm* realizes es.& ((((e'  L)
Thm* realizes es.& (((
Thm* realizes es.& (((isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
Thm* realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2))
Thm* realizes es.& ((& map(e'.<tag(e'),val(e')>;L)
Thm* realizes es.& ((& =
Thm* realizes es.& ((& tagged-list-messages(z.(z when e);val(e);f)
Thm* realizes es.& ((&  (tg:Idma-valtype(da; rcv(ltg))) List))
[better-sends-rule]
Thm* i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(dak)(da(rcv(ltg))?Void List)) List.
Thm* source(l) = i
Thm* 
Thm* d-single-sends(idsdaklf
Thm* realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id  (valtype(er ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (isrcv(e)
Thm* realizes es.& (
Thm* realizes es.& (lnk(e) = l  IdLnk
Thm* realizes es.& (
Thm* realizes es.& ((valtype(er ma-valtype(da; kind(e))))
Thm* realizes es.& ({m:Msg| source(mlnk(m)) = i } r Msg
Thm* realizes es.& (((l,tgda(rcv(ltg))?Top)))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = k  Knd
Thm* realizes es.& (
Thm* realizes es.& (sends(l;e)
Thm* realizes es.& (=
Thm* realizes es.& (tagged-messages(l;z.(z when e);val(e);f)
Thm* realizes es.& ( Msg((l,tgda(rcv(ltg))?Top)) List)
[sends-rule]
Thm* i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(State(ds)ma-valtype(dak)ds(x)?Void).
Thm* d-single-effect(idsdakxf
Thm* realizes es.(x:Id. vartype(i;xds(x)?Top)
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id  (valtype(er ma-valtype(da; kind(e))))
Thm* realizes es.& (e:E. 
Thm* realizes es.& (loc(e) = i  Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = k  Knd
Thm* realizes es.& (
Thm* realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top)
[effect-rule]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(tg:IdState(ds)ma-valtype(dak)(da(rcv(ltg))?Void List)) List.
Thm* xdom(ds). A=ds(x  A
Thm* 
Thm* kdom(da). A=da(k  A  Feasible(ma-single-sends(dsdaklf))
[ma-single-sends-feasible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
Thm* T
Thm* 
Thm* xdom(ds). A=ds(x  A
Thm* 
Thm* (s:State(ds). Dec(v:TP(s,v)))
Thm* 
Thm* Feasible((with ds: ds
Thm* Faction a:T
Thm* Fprecondition a(v) is
Thm* FP s v))
[ma-single-pre-feasible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm* f:(State(ds)ma-valtype(dak)ds(x)?Void).
Thm* xdom(ds). A=ds(x  A
Thm* 
Thm* kdom(da). A=da(k  A  Feasible(ma-single-effect(dsdakxf))
[ma-single-effect-feasible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp),
Thm* init:x:Id fp-> ds(x)?Void.
Thm* (with ds: ds init: initaction a:T precondition a(v) is P MsgA
[ma-single-pre-init_wf]

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