Def {i..j} == {k:| i  k < j }

is mentioned by

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

In prior sections: int 1 bool 1 int 2 list 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