let Values be Values_with_Bool; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: not simultev e1,e2
assume A0s: simultev e1,e2 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
then ( val r2w = the True of Values & Values is consistent ) by V1;
hence contradiction by Y2; :: thesis: verum
end;
hence ( r2 in tr & r2 reads turn, the True of Values ) by V2; :: thesis: 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 ; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st r2w in p by Y2;
then ( ( r2w in p1,tr or r2w in p2,tr ) & r2w writesto turn, the True of Values & Values is consistent ) by U1, Y2;
hence r2w in p1,tr by U3nw; :: thesis: verum
end;
( 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; :: thesis: verum
end;
hence r1 reads flag2, the False of Values by V1; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st wr2 in p by H1;
then ( ( wr2 in p1,tr or wr2 in p2,tr ) & wr2 writesto turn, the True of Values & Values is consistent ) by U1, H1;
hence wr2 in p1,tr by U3nw; :: thesis: verum
end;
M1: wr2 << r1 Q0: ( not u2 <= r1 or not r1 <= e2 )
proof
assume Q0a: ( u2 <= r1 & r1 <= e2 ) ; :: thesis: 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; :: thesis: verum
end;
then ( val r1w = the True of Values & Values is consistent ) by V2;
hence contradiction by Y2; :: thesis: 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; :: thesis: verum
end;
not r2 <= r1
proof
assume D0: r2 <= r1 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
then ( val r2w = the True of Values & Values is consistent ) by V2;
hence contradiction by Y2; :: thesis: verum
end;
hence ( r1 in tr & r1 reads turn, the False of Values ) by V1; :: thesis: 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 ; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st r2w in p by Y2;
then ( ( r2w in p2,tr or r2w in p1,tr ) & r2w writesto turn, the False of Values & Values is consistent ) by U1, Y2;
hence r2w in p2,tr by U3nw; :: thesis: verum
end;
( 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; :: thesis: verum
end;
hence r2 reads flag1, the False of Values by V2; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st wr2 in p by H1;
then ( ( wr2 in p2,tr or wr2 in p1,tr ) & wr2 writesto turn, the False of Values & Values is consistent ) by U1, H1;
hence wr2 in p2,tr by U3nw; :: thesis: verum
end;
M1: wr2 << r2 Q0: ( not u1 <= r2 or not r2 <= e1 )
proof
assume Q0a: ( u1 <= r2 & r2 <= e1 ) ; :: thesis: 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; :: thesis: verum
end;
then ( val r1w = the True of Values & Values is consistent ) by V1;
hence contradiction by Y2; :: thesis: 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; :: thesis: verum
end;
hence contradiction by thLinPreordEvents, RR1; :: thesis: 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 ) ; :: thesis: not simultev e1,e2
assume A0s: simultev e1,e2 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
then ( val r2w = the True of Values & Values is consistent ) by V1;
hence contradiction by Y2; :: thesis: verum
end;
hence ( r2 in tr & r2 reads turn, the False of Values ) by V2; :: thesis: 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 ; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st r2w in p by Y2;
then ( ( r2w in p2,tr or r2w in p1,tr ) & r2w writesto turn, the False of Values & Values is consistent ) by U1, Y2;
hence r2w in p2,tr by U3nw; :: thesis: verum
end;
( 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; :: thesis: verum
end;
hence r1 reads flag1, the False of Values by V1; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st wr2 in p by H1;
then ( ( wr2 in p2,tr or wr2 in p1,tr ) & wr2 writesto turn, the False of Values & Values is consistent ) by U1, H1;
hence wr2 in p2,tr by U3nw; :: thesis: verum
end;
M1: wr2 << r1 Q0: ( not u2 <= r1 or not r1 <= e2 )
proof
assume Q0a: ( u2 <= r1 & r1 <= e2 ) ; :: thesis: 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; :: thesis: verum
end;
then ( val r1w = the True of Values & Values is consistent ) by V2;
hence contradiction by Y2; :: thesis: 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; :: thesis: verum
end;
not r2 <= r1
proof
assume D0: r2 <= r1 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
then ( val r2w = the True of Values & Values is consistent ) by V2;
hence contradiction by Y2; :: thesis: verum
end;
hence ( r1 in tr & r1 reads turn, the True of Values ) by V1; :: thesis: 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 ; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st r2w in p by Y2;
then ( ( r2w in p1,tr or r2w in p2,tr ) & r2w writesto turn, the True of Values & Values is consistent ) by U1, Y2;
hence r2w in p1,tr by U3nw; :: thesis: verum
end;
( 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; :: thesis: verum
end;
hence r2 reads flag2, the False of Values by V2; :: thesis: 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
proof
DS is consistent ;
then DS is pr-complete ;
then ex p being Process of DS st wr2 in p by H1;
then ( ( wr2 in p1,tr or wr2 in p2,tr ) & wr2 writesto turn, the True of Values & Values is consistent ) by U1, H1;
hence wr2 in p1,tr by U3nw; :: thesis: verum
end;
M1: wr2 << r2 Q0: ( not u1 <= r2 or not r2 <= e1 )
proof
assume Q0a: ( u1 <= r2 & r2 <= e1 ) ; :: thesis: 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; :: thesis: verum
end;
then ( val r1w = the True of Values & Values is consistent ) by V1;
hence contradiction by Y2; :: thesis: 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; :: thesis: verum
end;
hence contradiction by thLinPreordEvents, RR1; :: thesis: verum
end;
hence ( e1 << e2 or e2 << e1 ) by thLinPreordEvents, W1, W2, U1, W3; :: thesis: verum