:: deftheorem defines rw-exclusive PETERSON:def 17 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-exclusive iff for e being Event of S
for x1, x2 being Location of S holds
( not e reads x1 or not e writesto x2 ) );