theorem :: PETERSON:15

for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for tr being trace of DS
for e1, e2 being Event of DS st e1 in tr & e2 in tr & {e1,e2} has_Peterson_mutex_in tr & not e1 = e2 & not e1 << e2 holds
e2 << e1