is mentioned by

Thm* the_w:World. FairFifo  Prop	[fair-fifo_wf]
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]

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 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