let Values be 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 )
let a1, a2 be 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 DS be 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 x be 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 tr be 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 e1, e2 be Event of DS; ( 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 )
; ( 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 )
; 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
;
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;
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; verum