:: deftheorem defines interval_in PETERSON:def 21 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS
for p being Process of DS
for tr being trace of DS holds (e1,e2) interval_in (p,tr) = { e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } ;