Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* B:(AType), f:x:A fp-> B(x). fpf-is-empty(f)  f =   x:A fp-> B(x)	[assert-fpf-is-empty]
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, l:IdLnk, t,t':. Thm* match(l;t;t') Thm*  Thm* ||snds(l;t)||||rcvs(l;t')|| Thm* & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||	[assert-w-match]
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-iff]
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, 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* es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e'	[assert-es-ble]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 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