mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ES
Def == E:Type
Def == EqDecider(E)(T:IdIdType
Def == EqDecider(E)(V:IdIdType
Def == EqDecider(E)(M:IdLnkIdType
Def == EqDecider(E)(Top(loc:EId
Def == EqDecider(E)(Top(kind:EKnd
Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e))
Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x))
Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x))
Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List))
Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e))
Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||)
Def == EqDecider(E)(Top(first:E
Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E
Def == EqDecider(E)(Top(causl:EEProp
Def == EqDecider(E)(Top(ESAxioms{i:l}
Def == EqDecider(E)(Top(ESAxioms(E;
Def == EqDecider(E)(Top(ESAxioms(T;
Def == EqDecider(E)(Top(ESAxioms(M;
Def == EqDecider(E)(Top(ESAxioms(loc;
Def == EqDecider(E)(Top(ESAxioms(kind;
Def == EqDecider(E)(Top(ESAxioms(val;
Def == EqDecider(E)(Top(ESAxioms(when;
Def == EqDecider(E)(Top(ESAxioms(after;
Def == EqDecider(E)(Top(ESAxioms(sends;
Def == EqDecider(E)(Top(ESAxioms(sender;
Def == EqDecider(E)(Top(ESAxioms(index;
Def == EqDecider(E)(Top(ESAxioms(first;
Def == EqDecider(E)(Top(ESAxioms(pred;
Def == EqDecider(E)(Top(ESAxioms(causl)
Def == EqDecider(E)(Top(Top))

is mentioned by

Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg)
Thm* 
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)		[es-kind-rcv]
Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l; tg)		[es-rcv-kind]
Thm* es:ES, x,i:Id, T:Type, c:T.
Thm* (x,y:T. Dec(x = y  T))
Thm* 
Thm* (vartype(i;x) r T)
Thm* 
Thm* (e:E. loc(e) = i  Id  first(e)  (x when e) = c  T)
Thm* 
Thm* (e':E. 
Thm* (loc(e') = i  Id
Thm* (
Thm* ((x after e') = c  T
Thm* (
Thm* ((ev:E. ev  e'  & (x after ev) = (x when ev)  T))		[change-since-init]
Thm* es:ES, e':E. e:E. first(e) & e  e' [es-first-exists]
Thm* es:ES, x,i:Id, T:Type.
Thm* (x,y:T. Dec(x = y  T))
Thm* 
Thm* (vartype(i;x) r T)
Thm* 
Thm* (e',e:E.
Thm* (e  e' 
Thm* (
Thm* (loc(e') = i  Id
Thm* (
Thm* ((x after e') = (x when e)  T
Thm* (
Thm* ((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T))		[change-lemma]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). e@i.P(e)  Prop[existse-at_wf]
Thm* es:ES, i,x:Id, T:Type, I:(TProp).
Thm* (vartype(i;x) r T) & e@i.first(e)  I((x when e))
Thm* 
Thm* e@i.I((x when e))  I((x after e))  @i always.I(x)		[es-invariant1]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop).
Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)		[alle-at-iff]
Thm* es:ES, x:Id, e:E.
Thm* first(e)  (x after pred(e)) = (x when e)  vartype(loc(e);x)		[es-after-pred]
Thm* the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e)  (Msg on l) List[es-tg-sends_wf]
Thm* the_es:ES, m:Msg. mlnk(m)  IdLnk[mlnk_wf2]
Thm* es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List[es-interval_wf2]
Thm* es:ES, e,e',ev:E. (ev  [e, e'])  e  ev  & ev  e' [member-es-interval]
Thm* the_es:ES, e',e:E. (e  before(e'))  (e <loc e')[member-es-before]
Thm* the_es:ES, e:E. before(e)  E List[es-before_wf]
Thm* the_es:ES, m:Msg. mtag(m)  Id[es-mtag_wf]
Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e' [assert-es-ble]
Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')  [es-ble_wf]

In prior sections: mb event system 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 3 Sections EventSystems Doc