let Values be 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
let DS be 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
let tr be 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
let e1, e2 be Event of DS; ( e1 in tr & e2 in tr & {e1,e2} has_Peterson_mutex_in tr & not e1 = e2 & not e1 << e2 implies e2 << e1 )
assume U0:
( e1 in tr & e2 in tr )
; ( not {e1,e2} has_Peterson_mutex_in tr or e1 = e2 or e1 << e2 or e2 << e1 )
assume
{e1,e2} has_Peterson_mutex_in tr
; ( e1 = e2 or e1 << e2 or e2 << e1 )
then consider p1, p2 being Process of DS such that
U1:
for p being Process of DS holds
( p = p1 or p = p2 )
and
U2:
ex flag1, flag2, turn being Location of DS st
( ( for e being Event of DS st e in p1,tr holds
( not e writesto flag2 & not e writesto turn, the False of Values ) ) & ( for e being Event of DS st e in p2,tr holds
( not e writesto flag1 & not e writesto turn, the True of Values ) ) & ( for e being Event of DS st e in {e1,e2} holds
( e has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr ) ) )
;
consider flag1, flag2, turn being Location of DS such that
U3nw:
( ( for e being Event of DS st e in p1,tr holds
( not e writesto flag2 & not e writesto turn, the False of Values ) ) & ( for e being Event of DS st e in p2,tr holds
( not e writesto flag1 & not e writesto turn, the True of Values ) ) )
and
U3:
for e being Event of DS st e in {e1,e2} holds
( e has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr )
by U2;
( {e1} c= {e1,e2} & {e2} c= {e1,e2} )
by ZFMISC_1:36;
then
( e1 in {e1,e2} & e2 in {e1,e2} )
by ZFMISC_1:31;
then U4:
( e1 has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e1 has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr & e2 has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e2 has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr )
by U3;
assume Aneq:
not e1 = e2
; ( e1 << e2 or e2 << e1 )
W1:
( ( not ( e1 in p1 & e2 in p1 ) & not ( e1 in p2 & e2 in p2 ) ) or e1 << e2 or e2 << e1 )
by Aneq, thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
DS is consistent
;
then
DS is pr-complete
;
then W2:
( ex p being Process of DS st e1 in p & ex p being Process of DS st e2 in p )
by U0;
W3:
( not e1 in p1 or not e2 in p2 or not simultev e1,e2 )
proof
assume A0:
(
e1 in p1 &
e2 in p2 )
;
not simultev e1,e2
assume A0s:
simultev e1,
e2
;
contradiction
consider u1,
w1,
r1 being
Event of
DS such that V1:
(
u1 in p1,
tr &
w1 in p1,
tr &
r1 in p1,
tr &
u1 < w1 &
w1 < r1 &
r1 < e1 &
u1 writesto flag1, the
True of
Values & not (
u1,
e1)
interval_in (
p1,
tr)
writesto flag1 &
w1 writesto turn, the
True of
Values & not (
w1,
e1)
interval_in (
p1,
tr)
writesto turn & (
r1 reads flag2, the
False of
Values or
r1 reads turn, the
False of
Values ) )
by U4;
V1o:
(
u1 << w1 &
w1 << r1 &
r1 << e1 )
by V1, A0, thEvStrictPrec;
consider u2,
w2,
r2 being
Event of
DS such that V2:
(
u2 in p2,
tr &
w2 in p2,
tr &
r2 in p2,
tr &
u2 < w2 &
w2 < r2 &
r2 < e2 &
u2 writesto flag2, the
True of
Values & not (
u2,
e2)
interval_in (
p2,
tr)
writesto flag2 &
w2 writesto turn, the
False of
Values & not (
w2,
e2)
interval_in (
p2,
tr)
writesto turn & (
r2 reads flag1, the
False of
Values or
r2 reads turn, the
True of
Values ) )
by U4;
V2o:
(
u2 << w2 &
w2 << r2 &
r2 << e2 )
by V2, A0, thEvStrictPrec;
RR1:
not
r1 <= r2
proof
assume D0:
r1 <= r2
;
contradiction
D01:
(
u1 << r2 &
r2 << e1 )
by V1o, thEvTrans, D0, A0s, V2, A0, thEvStrictPrec, thEvStrictTrans2;
D1:
(
r2 in tr &
r2 reads turn, the
True of
Values )
proof
not
r2 reads flag1, the
False of
Values
proof
assume Y1:
r2 reads flag1, the
False of
Values
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2w < r2 &
r2w writesto flag1 &
val r2w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r2 &
e writesto flag1 holds
e <= r2w ) )
by Y1, V2;
u1 = r2w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r2w in p
by Y2;
then TA01:
(
r2w in p1,
tr or
r2w in p2,
tr )
by U1, Y2;
TA02:
(
u1 < r2w &
r2w < e1 implies
r2w in (
u1,
e1)
interval_in (
p1,
tr) )
by U3nw, Y2, TA01;
TB01:
r2w << e1
by D01, thEvStrictTrans1, ORDERS_2:def 6, Y2;
(
u1 in p1,
tr &
r2w in p1,
tr & not
u1 << r2w )
by TB01, Y2, TA02, TA01, U3nw, V1, ORDERS_2:def 6;
then
(
u1 = r2w or
r2w << u1 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u1 = r2w
by Y2, V1, D01;
verum
end;
then
(
val r2w = the
True of
Values &
Values is
consistent )
by V1;
hence
contradiction
by Y2;
verum
end;
hence
(
r2 in tr &
r2 reads turn, the
True of
Values )
by V2;
verum
end;
D2:
r1 reads flag2, the
False of
Values
proof
not
r1 reads turn, the
False of
Values
proof
assume Y1:
r1 reads turn, the
False of
Values
;
contradiction
Values is
consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r1 << r2w &
r2w << r2 &
r2w writesto turn, the
True of
Values )
by lemwbefr, V1, D1, D0, Y1;
Y3:
r2w in p1,
tr
(
r2w << r2 &
r2 <= e2 )
by ORDERS_2:def 6, Y2, V2;
then IA0:
r2w << e2
by thEvTrans;
IB0:
(
w1 <= r1 &
r1 << r2w )
by Y2, V1, ORDERS_2:def 6;
(
w1 < r2w &
r2w < e1 )
by thEvTrans, A0s, IA0, IB0, ORDERS_2:def 6;
then
r2w in (
w1,
e1)
interval_in (
p1,
tr)
by Y3;
hence
contradiction
by V1, Y2;
verum
end;
hence
r1 reads flag2, the
False of
Values
by V1;
verum
end;
DS is
consistent
;
then
DS is
rw-consistent
;
then consider wr2 being
Event of
DS such that H1:
(
wr2 in tr &
wr2 < r2 &
wr2 writesto turn &
val wr2 = the
True of
Values & ( for
e1 being
Event of
DS st
e1 in tr &
e1 <= r2 &
e1 writesto turn holds
e1 <= wr2 ) )
by D1;
H2:
wr2 in p1,
tr
M1:
wr2 << r1
proof
r2 << e1
by V2, A0, thEvStrictPrec, A0s, thEvStrictTrans2;
then J1:
wr2 << e1
by ORDERS_2:def 6, H1, thEvStrictTrans1;
J2:
not
r1 << wr2
DS is
consistent
;
then J30:
DS is
pr-ordered
;
DS is
consistent
;
then
DS is
rw-exclusive
;
then
not
r1 = wr2
by D2, H1;
hence
wr2 << r1
by J2, H2, V1, thLinPreordEvents, J30;
verum
end;
Q0:
( not
u2 <= r1 or not
r1 <= e2 )
proof
assume Q0a:
(
u2 <= r1 &
r1 <= e2 )
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r1w being
Event of
DS such that Y2:
(
r1w in tr &
r1w < r1 &
r1w writesto flag2 &
val r1w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r1 &
e writesto flag2 holds
e <= r1w ) )
by V1, D2;
u2 = r1w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r1w in p
by Y2;
then TA01:
(
r1w in p1,
tr or
r1w in p2,
tr )
by U1, Y2;
TA02:
(
u2 < r1w &
r1w < e2 implies
r1w in (
u2,
e2)
interval_in (
p2,
tr) )
by TA01, U3nw, Y2;
(
r1w <= r1 &
r1 << e1 )
by V1, A0, thEvStrictPrec, Y2, ORDERS_2:def 6;
then
(
r1w <= r1 &
r1 << e2 )
by A0s, thEvTrans;
then
(
u2 in p2,
tr &
r1w in p2,
tr & not
u2 << r1w )
by Y2, TA01, U3nw, V2, TA02, thEvTrans, ORDERS_2:def 6;
then
(
u2 = r1w or
r1w << u2 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u2 = r1w
by Y2, V2, Q0a;
verum
end;
then
(
val r1w = the
True of
Values &
Values is
consistent )
by V2;
hence
contradiction
by Y2;
verum
end;
M20:
r1 << e1
by V1, A0, thEvStrictPrec;
(
u2 << w2 &
w2 <= wr2 &
wr2 << r1 )
by M1, V2, thEvStrictPrec, H1, ORDERS_2:def 6;
then
(
u2 << wr2 &
wr2 << r1 )
by thEvTrans;
hence
contradiction
by M20, Q0, A0s, thEvTrans;
verum
end;
not
r2 <= r1
proof
assume D0:
r2 <= r1
;
contradiction
D01:
(
u2 << r1 &
r1 << e2 )
by V2o, thEvTrans, D0, A0s, V1, A0, thEvStrictPrec, thEvStrictTrans2;
D1:
(
r1 in tr &
r1 reads turn, the
False of
Values )
proof
not
r1 reads flag2, the
False of
Values
proof
assume Y1:
r1 reads flag2, the
False of
Values
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2w < r1 &
r2w writesto flag2 &
val r2w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r1 &
e writesto flag2 holds
e <= r2w ) )
by Y1, V1;
u2 = r2w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r2w in p
by Y2;
then TA01:
(
r2w in p2,
tr or
r2w in p1,
tr )
by U1, Y2;
TA02:
(
u2 < r2w &
r2w < e2 implies
r2w in (
u2,
e2)
interval_in (
p2,
tr) )
by U3nw, Y2, TA01;
TB01:
r2w << e2
by D01, thEvStrictTrans1, ORDERS_2:def 6, Y2;
(
u2 in p2,
tr &
r2w in p2,
tr & not
u2 << r2w )
by TB01, Y2, TA02, TA01, U3nw, V2, ORDERS_2:def 6;
then
(
u2 = r2w or
r2w << u2 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u2 = r2w
by Y2, V2, D01;
verum
end;
then
(
val r2w = the
True of
Values &
Values is
consistent )
by V2;
hence
contradiction
by Y2;
verum
end;
hence
(
r1 in tr &
r1 reads turn, the
False of
Values )
by V1;
verum
end;
D2:
r2 reads flag1, the
False of
Values
proof
not
r2 reads turn, the
True of
Values
proof
assume Y1:
r2 reads turn, the
True of
Values
;
contradiction
Values is
consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2 << r2w &
r2w << r1 &
r2w writesto turn, the
False of
Values )
by lemwbefr, V2, D1, D0, Y1;
Y3:
r2w in p2,
tr
(
r2w << r1 &
r1 <= e1 )
by ORDERS_2:def 6, Y2, V1;
then IA0:
r2w << e1
by thEvTrans;
IB0:
(
w2 <= r2 &
r2 << r2w )
by Y2, V2, ORDERS_2:def 6;
(
w2 < r2w &
r2w < e2 )
by thEvTrans, A0s, IA0, IB0, ORDERS_2:def 6;
then
r2w in (
w2,
e2)
interval_in (
p2,
tr)
by Y3;
hence
contradiction
by V2, Y2;
verum
end;
hence
r2 reads flag1, the
False of
Values
by V2;
verum
end;
DS is
consistent
;
then
DS is
rw-consistent
;
then consider wr2 being
Event of
DS such that H1:
(
wr2 in tr &
wr2 < r1 &
wr2 writesto turn &
val wr2 = the
False of
Values & ( for
e2 being
Event of
DS st
e2 in tr &
e2 <= r1 &
e2 writesto turn holds
e2 <= wr2 ) )
by D1;
H2:
wr2 in p2,
tr
M1:
wr2 << r2
proof
r1 << e2
by V1, A0, thEvStrictPrec, A0s, thEvStrictTrans2;
then J1:
wr2 << e2
by ORDERS_2:def 6, H1, thEvStrictTrans1;
J2:
not
r2 << wr2
DS is
consistent
;
then J30:
DS is
pr-ordered
;
DS is
consistent
;
then
DS is
rw-exclusive
;
then
not
r2 = wr2
by D2, H1;
hence
wr2 << r2
by J2, H2, V2, thLinPreordEvents, J30;
verum
end;
Q0:
( not
u1 <= r2 or not
r2 <= e1 )
proof
assume Q0a:
(
u1 <= r2 &
r2 <= e1 )
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r1w being
Event of
DS such that Y2:
(
r1w in tr &
r1w < r2 &
r1w writesto flag1 &
val r1w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r2 &
e writesto flag1 holds
e <= r1w ) )
by V2, D2;
u1 = r1w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r1w in p
by Y2;
then TA01:
(
r1w in p2,
tr or
r1w in p1,
tr )
by U1, Y2;
TA02:
(
u1 < r1w &
r1w < e1 implies
r1w in (
u1,
e1)
interval_in (
p1,
tr) )
by TA01, U3nw, Y2;
(
r1w <= r2 &
r2 << e2 )
by V2, A0, thEvStrictPrec, Y2, ORDERS_2:def 6;
then
(
r1w <= r2 &
r2 << e1 )
by A0s, thEvTrans;
then
(
u1 in p1,
tr &
r1w in p1,
tr & not
u1 << r1w )
by Y2, TA01, U3nw, V1, TA02, thEvTrans, ORDERS_2:def 6;
then
(
u1 = r1w or
r1w << u1 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u1 = r1w
by Y2, V1, Q0a;
verum
end;
then
(
val r1w = the
True of
Values &
Values is
consistent )
by V1;
hence
contradiction
by Y2;
verum
end;
M20:
r2 << e1
by V2, A0s, A0, thEvStrictPrec, thEvStrictTrans2;
(
u1 << w1 &
w1 <= wr2 &
wr2 << r2 )
by M1, thEvStrictPrec, V1, H1, ORDERS_2:def 6;
then
(
u1 << wr2 &
wr2 << r2 )
by thEvTrans;
hence
contradiction
by M20, Q0, thEvTrans;
verum
end;
hence
contradiction
by thLinPreordEvents, RR1;
verum
end;
( not e1 in p2 or not e2 in p1 or not simultev e1,e2 )
proof
assume A0:
(
e1 in p2 &
e2 in p1 )
;
not simultev e1,e2
assume A0s:
simultev e1,
e2
;
contradiction
consider u1,
w1,
r1 being
Event of
DS such that V1:
(
u1 in p2,
tr &
w1 in p2,
tr &
r1 in p2,
tr &
u1 < w1 &
w1 < r1 &
r1 < e1 &
u1 writesto flag2, the
True of
Values & not (
u1,
e1)
interval_in (
p2,
tr)
writesto flag2 &
w1 writesto turn, the
False of
Values & not (
w1,
e1)
interval_in (
p2,
tr)
writesto turn & (
r1 reads flag1, the
False of
Values or
r1 reads turn, the
True of
Values ) )
by U4;
V1o:
(
u1 << w1 &
w1 << r1 &
r1 << e1 )
by V1, A0, thEvStrictPrec;
consider u2,
w2,
r2 being
Event of
DS such that V2:
(
u2 in p1,
tr &
w2 in p1,
tr &
r2 in p1,
tr &
u2 < w2 &
w2 < r2 &
r2 < e2 &
u2 writesto flag1, the
True of
Values & not (
u2,
e2)
interval_in (
p1,
tr)
writesto flag1 &
w2 writesto turn, the
True of
Values & not (
w2,
e2)
interval_in (
p1,
tr)
writesto turn & (
r2 reads flag2, the
False of
Values or
r2 reads turn, the
False of
Values ) )
by U4;
V2o:
(
u2 << w2 &
w2 << r2 &
r2 << e2 )
by V2, A0, thEvStrictPrec;
RR1:
not
r1 <= r2
proof
assume D0:
r1 <= r2
;
contradiction
D01:
(
u1 << r2 &
r2 << e1 )
by V1o, thEvTrans, D0, A0s, V2, A0, thEvStrictPrec, thEvStrictTrans2;
D1:
(
r2 in tr &
r2 reads turn, the
False of
Values )
proof
not
r2 reads flag2, the
False of
Values
proof
assume Y1:
r2 reads flag2, the
False of
Values
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2w < r2 &
r2w writesto flag2 &
val r2w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r2 &
e writesto flag2 holds
e <= r2w ) )
by Y1, V2;
u1 = r2w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r2w in p
by Y2;
then TA01:
(
r2w in p2,
tr or
r2w in p1,
tr )
by U1, Y2;
TA02:
(
u1 < r2w &
r2w < e1 implies
r2w in (
u1,
e1)
interval_in (
p2,
tr) )
by U3nw, Y2, TA01;
TB01:
r2w << e1
by D01, thEvStrictTrans1, ORDERS_2:def 6, Y2;
(
u1 in p2,
tr &
r2w in p2,
tr & not
u1 << r2w )
by TB01, Y2, TA02, TA01, U3nw, V1, ORDERS_2:def 6;
then
(
u1 = r2w or
r2w << u1 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u1 = r2w
by Y2, V1, D01;
verum
end;
then
(
val r2w = the
True of
Values &
Values is
consistent )
by V1;
hence
contradiction
by Y2;
verum
end;
hence
(
r2 in tr &
r2 reads turn, the
False of
Values )
by V2;
verum
end;
D2:
r1 reads flag1, the
False of
Values
proof
not
r1 reads turn, the
True of
Values
proof
assume Y1:
r1 reads turn, the
True of
Values
;
contradiction
Values is
consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r1 << r2w &
r2w << r2 &
r2w writesto turn, the
False of
Values )
by lemwbefr, V1, D1, D0, Y1;
Y3:
r2w in p2,
tr
(
r2w << r2 &
r2 <= e2 )
by ORDERS_2:def 6, Y2, V2;
then IA0:
r2w << e2
by thEvTrans;
IB0:
(
w1 <= r1 &
r1 << r2w )
by Y2, V1, ORDERS_2:def 6;
(
w1 < r2w &
r2w < e1 )
by thEvTrans, A0s, IA0, IB0, ORDERS_2:def 6;
then
r2w in (
w1,
e1)
interval_in (
p2,
tr)
by Y3;
hence
contradiction
by V1, Y2;
verum
end;
hence
r1 reads flag1, the
False of
Values
by V1;
verum
end;
DS is
consistent
;
then
DS is
rw-consistent
;
then consider wr2 being
Event of
DS such that H1:
(
wr2 in tr &
wr2 < r2 &
wr2 writesto turn &
val wr2 = the
False of
Values & ( for
e1 being
Event of
DS st
e1 in tr &
e1 <= r2 &
e1 writesto turn holds
e1 <= wr2 ) )
by D1;
H2:
wr2 in p2,
tr
M1:
wr2 << r1
proof
r2 << e1
by V2, A0, thEvStrictPrec, A0s, thEvStrictTrans2;
then J1:
wr2 << e1
by ORDERS_2:def 6, H1, thEvStrictTrans1;
J2:
not
r1 << wr2
DS is
consistent
;
then J30:
DS is
pr-ordered
;
DS is
consistent
;
then
DS is
rw-exclusive
;
then
not
r1 = wr2
by D2, H1;
hence
wr2 << r1
by J2, H2, V1, thLinPreordEvents, J30;
verum
end;
Q0:
( not
u2 <= r1 or not
r1 <= e2 )
proof
assume Q0a:
(
u2 <= r1 &
r1 <= e2 )
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r1w being
Event of
DS such that Y2:
(
r1w in tr &
r1w < r1 &
r1w writesto flag1 &
val r1w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r1 &
e writesto flag1 holds
e <= r1w ) )
by V1, D2;
u2 = r1w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r1w in p
by Y2;
then TA01:
(
r1w in p2,
tr or
r1w in p1,
tr )
by U1, Y2;
TA02:
(
u2 < r1w &
r1w < e2 implies
r1w in (
u2,
e2)
interval_in (
p1,
tr) )
by TA01, U3nw, Y2;
(
r1w <= r1 &
r1 << e1 )
by V1, A0, thEvStrictPrec, Y2, ORDERS_2:def 6;
then
(
r1w <= r1 &
r1 << e2 )
by A0s, thEvTrans;
then
(
u2 in p1,
tr &
r1w in p1,
tr & not
u2 << r1w )
by Y2, TA01, U3nw, V2, TA02, thEvTrans, ORDERS_2:def 6;
then
(
u2 = r1w or
r1w << u2 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u2 = r1w
by Y2, V2, Q0a;
verum
end;
then
(
val r1w = the
True of
Values &
Values is
consistent )
by V2;
hence
contradiction
by Y2;
verum
end;
M20:
r1 << e1
by V1, A0, thEvStrictPrec;
(
u2 << w2 &
w2 <= wr2 &
wr2 << r1 )
by M1, V2, thEvStrictPrec, H1, ORDERS_2:def 6;
then
(
u2 << wr2 &
wr2 << r1 )
by thEvTrans;
hence
contradiction
by M20, Q0, A0s, thEvTrans;
verum
end;
not
r2 <= r1
proof
assume D0:
r2 <= r1
;
contradiction
D01:
(
u2 << r1 &
r1 << e2 )
by V2o, thEvTrans, D0, A0s, V1, A0, thEvStrictPrec, thEvStrictTrans2;
D1:
(
r1 in tr &
r1 reads turn, the
True of
Values )
proof
not
r1 reads flag1, the
False of
Values
proof
assume Y1:
r1 reads flag1, the
False of
Values
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2w < r1 &
r2w writesto flag1 &
val r2w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r1 &
e writesto flag1 holds
e <= r2w ) )
by Y1, V1;
u2 = r2w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r2w in p
by Y2;
then TA01:
(
r2w in p1,
tr or
r2w in p2,
tr )
by U1, Y2;
TA02:
(
u2 < r2w &
r2w < e2 implies
r2w in (
u2,
e2)
interval_in (
p1,
tr) )
by U3nw, Y2, TA01;
TB01:
r2w << e2
by D01, thEvStrictTrans1, ORDERS_2:def 6, Y2;
(
u2 in p1,
tr &
r2w in p1,
tr & not
u2 << r2w )
by TB01, Y2, TA02, TA01, U3nw, V2, ORDERS_2:def 6;
then
(
u2 = r2w or
r2w << u2 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u2 = r2w
by Y2, V2, D01;
verum
end;
then
(
val r2w = the
True of
Values &
Values is
consistent )
by V2;
hence
contradiction
by Y2;
verum
end;
hence
(
r1 in tr &
r1 reads turn, the
True of
Values )
by V1;
verum
end;
D2:
r2 reads flag2, the
False of
Values
proof
not
r2 reads turn, the
False of
Values
proof
assume Y1:
r2 reads turn, the
False of
Values
;
contradiction
Values is
consistent
;
then consider r2w being
Event of
DS such that Y2:
(
r2w in tr &
r2 << r2w &
r2w << r1 &
r2w writesto turn, the
True of
Values )
by lemwbefr, V2, D1, D0, Y1;
Y3:
r2w in p1,
tr
(
r2w << r1 &
r1 <= e1 )
by ORDERS_2:def 6, Y2, V1;
then IA0:
r2w << e1
by thEvTrans;
IB0:
(
w2 <= r2 &
r2 << r2w )
by Y2, V2, ORDERS_2:def 6;
(
w2 < r2w &
r2w < e2 )
by thEvTrans, A0s, IA0, IB0, ORDERS_2:def 6;
then
r2w in (
w2,
e2)
interval_in (
p1,
tr)
by Y3;
hence
contradiction
by V2, Y2;
verum
end;
hence
r2 reads flag2, the
False of
Values
by V2;
verum
end;
DS is
consistent
;
then
DS is
rw-consistent
;
then consider wr2 being
Event of
DS such that H1:
(
wr2 in tr &
wr2 < r1 &
wr2 writesto turn &
val wr2 = the
True of
Values & ( for
e2 being
Event of
DS st
e2 in tr &
e2 <= r1 &
e2 writesto turn holds
e2 <= wr2 ) )
by D1;
H2:
wr2 in p1,
tr
M1:
wr2 << r2
proof
r1 << e2
by V1, A0, thEvStrictPrec, A0s, thEvStrictTrans2;
then J1:
wr2 << e2
by ORDERS_2:def 6, H1, thEvStrictTrans1;
J2:
not
r2 << wr2
DS is
consistent
;
then J30:
DS is
pr-ordered
;
DS is
consistent
;
then
DS is
rw-exclusive
;
then
not
r2 = wr2
by D2, H1;
hence
wr2 << r2
by J2, H2, V2, thLinPreordEvents, J30;
verum
end;
Q0:
( not
u1 <= r2 or not
r2 <= e1 )
proof
assume Q0a:
(
u1 <= r2 &
r2 <= e1 )
;
contradiction
DS is
consistent
;
then
DS is
rw-consistent
;
then consider r1w being
Event of
DS such that Y2:
(
r1w in tr &
r1w < r2 &
r1w writesto flag2 &
val r1w = the
False of
Values & ( for
e being
Event of
DS st
e in tr &
e <= r2 &
e writesto flag2 holds
e <= r1w ) )
by V2, D2;
u1 = r1w
proof
DS is
consistent
;
then
DS is
pr-complete
;
then
ex
p being
Process of
DS st
r1w in p
by Y2;
then TA01:
(
r1w in p1,
tr or
r1w in p2,
tr )
by U1, Y2;
TA02:
(
u1 < r1w &
r1w < e1 implies
r1w in (
u1,
e1)
interval_in (
p2,
tr) )
by TA01, U3nw, Y2;
(
r1w <= r2 &
r2 << e2 )
by V2, A0, thEvStrictPrec, Y2, ORDERS_2:def 6;
then
(
r1w <= r2 &
r2 << e1 )
by A0s, thEvTrans;
then
(
u1 in p2,
tr &
r1w in p2,
tr & not
u1 << r1w )
by Y2, TA01, U3nw, V1, TA02, thEvTrans, ORDERS_2:def 6;
then
(
u1 = r1w or
r1w << u1 )
by thLinPreordEvents, thEvStrictPrec, ORDERS_2:def 6;
hence
u1 = r1w
by Y2, V1, Q0a;
verum
end;
then
(
val r1w = the
True of
Values &
Values is
consistent )
by V1;
hence
contradiction
by Y2;
verum
end;
M20:
r2 << e1
by V2, A0s, A0, thEvStrictPrec, thEvStrictTrans2;
(
u1 << w1 &
w1 <= wr2 &
wr2 << r2 )
by M1, thEvStrictPrec, V1, H1, ORDERS_2:def 6;
then
(
u1 << wr2 &
wr2 << r2 )
by thEvTrans;
hence
contradiction
by M20, Q0, thEvTrans;
verum
end;
hence
contradiction
by thLinPreordEvents, RR1;
verum
end;
hence
( e1 << e2 or e2 << e1 )
by thLinPreordEvents, W1, W2, U1, W3; verum