mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P  Q == PQ

is mentioned by

Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A.
Thm* x  dom(f)  f(x)  B(x)		[fpf-ap_wf]
Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
Thm* strong-subtype(X;Y)  x  dom(f)  x  X		[fpf-dom-type2]
Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
Thm* strong-subtype(X;Y)  x  dom(f)  x  X		[fpf-dom-type]
Thm* eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x  dom(f)  x  dom(f)[fpf-dom_functionality2]
Thm* B1:(A1Type), B2:(A2Type).
Thm* strong-subtype(A1;A2)
Thm* 
Thm* (a:A1. B1(a) r B2(a))  (a:A1 fp-> B1(a) r a:A2 fp-> B2(a))		[subtype-fpf3]
Thm* B1,B2:(AType).
Thm* (a:A. B1(a) r B2(a))  (a:A fp-> B1(a) r a:A fp-> B2(a))		[subtype-fpf2]
Thm* i:Id, w:World, p:FairFifo, t:.
Thm* isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t)))		[es-valtype-w-valtype]
Thm* the_w:World. 
Thm* FairFifo
Thm* 
Thm* ESAxioms{i:l}
Thm* ESAxioms(E;
Thm* ESAxioms((i,x. vartype(i;x));
Thm* ESAxioms(the_w.M;
Thm* ESAxioms((e.loc(e));
Thm* ESAxioms((e.kind(e));
Thm* ESAxioms((e.val(e));
Thm* ESAxioms((x,e. (x when e));
Thm* ESAxioms((x,e. (x after e));
Thm* ESAxioms((l,e. sends(l;e));
Thm* ESAxioms((e.sender(e));
Thm* ESAxioms((e.index(e));
Thm* ESAxioms((e.first(e));
Thm* ESAxioms((e.pred(e));
Thm* ESAxioms((e,e'. e <c e'))		[world-event-system]
Thm* the_w:World, e,e':E.
Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')		[w-locl-iff]
Thm* the_w:World, e,e':E. FairFifo  e <c e'  time(e)<time(e')[w-causl-time]
Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))||		[w-index_wf]
Thm* the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E[w-sender_wf]
Thm* the_w:World, e:E, t:.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))
Thm* 
Thm* onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
Thm* -||snds(lnk(kind(e));t)||)]
Thm* =
Thm* msg(a(loc(e);time(e)))
Thm*  Msg		[w-match-property]
Thm* the_w:World, e:E, t,t':.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'		[w-match-unique]
Thm* the_w:World, e:E.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* (t:time(e). 
Thm* (match(lnk(kind(e));t;time(e))
Thm* (& onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
Thm* (& -||snds(lnk(kind(e));t)||)]
Thm* (& =
Thm* (& msg(a(loc(e);time(e)))
Thm* (&  Msg)		[better-w-match-exists]
Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))		[w-match-exists]
Thm* the_w:World, e:E. first(e)  pred(e)  E[w-pred_wf]
Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E[w-pred-aux]
Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))[assert-w-first]
Thm* the_w:World, e,e':E. e = e'  e = e'[assert-w-eq-E]
Thm* the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a)  msg(a)  Msg[w-msg_wf]
Thm* the_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a)  isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l		[assert-w-isrcvl]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  val(a)  valtype(i;a)[w-val_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  valtype(i;a)  Type[w-valtype_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  kind(a)  Knd[w-kind_wf]
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, 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,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]
Def f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)[fpf-sub]
Def z != f(x) ==> P(a;z) == x  dom(f)  P(x;f(x))[fpf-val]
Def 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)		[fair-fifo]
Def e@i.P(e) == e:E. loc(e) = i  Id  P(e)[alle-at]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 sqequal 1 union mb basic mb nat mb list 1 num thy 1 mb list 2 mb event system 1 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