:: deftheorem defines simultev PETERSON:def 22 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( simultev e1,e2 iff ( e1 <= e2 & e2 <= e1 ) );