:: deftheorem defines rw-ordered PETERSON:def 15 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-ordered iff for x being Location of S
for e1, e2 being Event of S st ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 holds
e1 = e2 );