:: deftheorem defines rw-consistent PETERSON:def 16 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is rw-consistent iff for tr being trace of S
for x being Location of S
for e being Event of S
for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds
ex e0 being Event of S st
( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of S st e1 in tr & e1 <= e & e1 writesto x holds
e1 <= e0 ) ) );