theorem lemwbefr: :: PETERSON:14

for Values being Values_with_Bool
for a1, a2 being Element of the carrier of Values
for DS being DistributedSysWithSharedMem of Values
for x being Location of DS
for tr being trace of DS
for e1, e2 being Event of DS st e1 in tr & e2 in tr & e1 reads x,a1 & e2 reads x,a2 & e1 <= e2 & a1 <> a2 holds
ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 )