let Values be Values_with_Bool; :: thesis: 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 )
let a1, a2 be Element of the carrier of Values; :: thesis: 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 )
let DS be DistributedSysWithSharedMem of Values; :: thesis: 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 )
let x be Location of DS; :: thesis: 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 )
let tr be trace of DS; :: thesis: 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 )
let e1, e2 be Event of DS; :: thesis: ( e1 in tr & e2 in tr & e1 reads x,a1 & e2 reads x,a2 & e1 <= e2 & a1 <> a2 implies ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 ) )
assume A0: ( e1 in tr & e2 in tr ) ; :: thesis: ( not e1 reads x,a1 or not e2 reads x,a2 or not e1 <= e2 or not a1 <> a2 or ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 ) )
assume A1: ( e1 reads x,a1 & e2 reads x,a2 & e1 <= e2 & a1 <> a2 ) ; :: thesis: ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 )
DS is consistent ;
then DS is rw-consistent ;
then consider e2w being Event of DS such that
B1: ( e2w in tr & e2w < e2 & e2w writesto x & val e2w = a2 & ( for e being Event of DS st e in tr & e <= e2 & e writesto x holds
e <= e2w ) ) by A0, A1;
DS is consistent ;
then JJ0: DS is rw-ordered ;
C1: not e2w << e1

proof

assume D1: e2w << e1 ; :: thesis: contradiction
DS is consistent ;
then DS is rw-consistent ;
then consider e1w being Event of DS such that
D2: ( e1w in tr & e1w < e1 & e1w writesto x & val e1w = a1 & ( for e being Event of DS st e in tr & e <= e1 & e writesto x holds
e <= e1w ) ) by A0, A1;
D3: e2w <= e1w by D1, D2, B1;
( e1w <= e1 & e1 <= e2 ) by A1, D2, ORDERS_2:def 6;
then e1w <= e2 by thEvTrans;
then D4: e1w <= e2w by B1, D2;
DS is consistent ;
then DS is rw-ordered ;
hence contradiction by B1, D2, A1, D3, D4; :: thesis: verum

end;

C2: not e2 << e2w by B1, ORDERS_2:def 6;
( e1 << e2w & e2w << e2 & e2w writesto x,a2 ) by thLinPreordEvents, JJ0, A1, C1, C2, B1;
hence ex e being Event of DS st
( e in tr & e1 << e & e << e2 & e writesto x,a2 ) by B1; :: thesis: verum