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 )

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

( not e1 in p2 or not e2 in p1 or not simultev e1,e2 )
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

end;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

not r2 <= r1
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 )

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

( 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;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

D2:
r1 reads flag2, the False of Values
not r2 reads flag1, the False of Values

end;proof

hence
( r2 in tr & r2 reads turn, the True of Values )
by V2; :: thesis: verum
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r2w = the True of Values & Values is consistent )
by V1;
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 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

hence contradiction by Y2; :: thesis: verum

proof

DS is consistent
;
not r1 reads turn, the False of Values

end;proof

hence
r1 reads flag2, the False of Values
by V1; :: thesis: verum
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

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;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

( r2w << r2 & r2 <= e2 )
by ORDERS_2:def 6, Y2, V2;
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;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

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

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

M1:
wr2 << r1
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;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

proof

Q0:
( not u2 <= r1 or not r1 <= e2 )
r2 << e1
by V2, A0, thEvStrictPrec, A0s, thEvStrictTrans2;

then J1: wr2 << e1 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r1 << wr2

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; :: thesis: verum

end;then J1: wr2 << e1 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r1 << wr2

proof

DS is consistent
;
assume
r1 << wr2
; :: thesis: contradiction

then ( w1 << wr2 & wr2 < e1 ) by ORDERS_2:def 6, J1, V1, thEvStrictTrans1;

then ( w1 < wr2 & wr2 < e1 ) by ORDERS_2:def 6;

then wr2 in (w1,e1) interval_in (p1,tr) by H2;

hence contradiction by V1, H1; :: thesis: verum

end;then ( w1 << wr2 & wr2 < e1 ) by ORDERS_2:def 6, J1, V1, thEvStrictTrans1;

then ( w1 < wr2 & wr2 < e1 ) by ORDERS_2:def 6;

then wr2 in (w1,e1) interval_in (p1,tr) by H2;

hence contradiction by V1, H1; :: thesis: verum

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; :: thesis: verum

proof

M20:
r1 << e1
by V1, A0, thEvStrictPrec;
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r1w = the True of Values & Values is consistent )
by V2;
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 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

hence contradiction by Y2; :: thesis: verum

( 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

proof

hence
contradiction
by thLinPreordEvents, RR1; :: thesis: verum
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 )

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

( 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;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

D2:
r2 reads flag1, the False of Values
not r1 reads flag2, the False of Values

end;proof

hence
( r1 in tr & r1 reads turn, the False of Values )
by V1; :: thesis: verum
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r2w = the True of Values & Values is consistent )
by V2;
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 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

hence contradiction by Y2; :: thesis: verum

proof

DS is consistent
;
not r2 reads turn, the True of Values

end;proof

hence
r2 reads flag1, the False of Values
by V2; :: thesis: verum
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

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;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

( r2w << r1 & r1 <= e1 )
by ORDERS_2:def 6, Y2, V1;
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;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

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

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

M1:
wr2 << r2
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;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

proof

Q0:
( not u1 <= r2 or not r2 <= e1 )
r1 << e2
by V1, A0, thEvStrictPrec, A0s, thEvStrictTrans2;

then J1: wr2 << e2 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r2 << wr2

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; :: thesis: verum

end;then J1: wr2 << e2 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r2 << wr2

proof

DS is consistent
;
assume
r2 << wr2
; :: thesis: contradiction

then ( w2 << wr2 & wr2 < e2 ) by ORDERS_2:def 6, J1, V2, thEvStrictTrans1;

then ( w2 < wr2 & wr2 < e2 ) by ORDERS_2:def 6;

then wr2 in (w2,e2) interval_in (p2,tr) by H2;

hence contradiction by V2, H1; :: thesis: verum

end;then ( w2 << wr2 & wr2 < e2 ) by ORDERS_2:def 6, J1, V2, thEvStrictTrans1;

then ( w2 < wr2 & wr2 < e2 ) by ORDERS_2:def 6;

then wr2 in (w2,e2) interval_in (p2,tr) by H2;

hence contradiction by V2, H1; :: thesis: verum

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; :: thesis: verum

proof

M20:
r2 << e1
by V2, A0s, A0, thEvStrictPrec, thEvStrictTrans2;
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r1w = the True of Values & Values is consistent )
by V1;
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 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

hence contradiction by Y2; :: thesis: verum

( 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

proof

hence
( e1 << e2 or e2 << e1 )
by thLinPreordEvents, W1, W2, U1, W3; :: thesis: verum
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

end;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

not r2 <= r1
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 )

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

( 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;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

D2:
r1 reads flag1, the False of Values
not r2 reads flag2, the False of Values

end;proof

hence
( r2 in tr & r2 reads turn, the False of Values )
by V2; :: thesis: verum
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r2w = the True of Values & Values is consistent )
by V1;
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 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

hence contradiction by Y2; :: thesis: verum

proof

DS is consistent
;
not r1 reads turn, the True of Values

end;proof

hence
r1 reads flag1, the False of Values
by V1; :: thesis: verum
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

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;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

( r2w << r2 & r2 <= e2 )
by ORDERS_2:def 6, Y2, V2;
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;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

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

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

M1:
wr2 << r1
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;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

proof

Q0:
( not u2 <= r1 or not r1 <= e2 )
r2 << e1
by V2, A0, thEvStrictPrec, A0s, thEvStrictTrans2;

then J1: wr2 << e1 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r1 << wr2

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; :: thesis: verum

end;then J1: wr2 << e1 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r1 << wr2

proof

DS is consistent
;
assume
r1 << wr2
; :: thesis: contradiction

then ( w1 << wr2 & wr2 < e1 ) by ORDERS_2:def 6, J1, V1, thEvStrictTrans1;

then ( w1 < wr2 & wr2 < e1 ) by ORDERS_2:def 6;

then wr2 in (w1,e1) interval_in (p2,tr) by H2;

hence contradiction by V1, H1; :: thesis: verum

end;then ( w1 << wr2 & wr2 < e1 ) by ORDERS_2:def 6, J1, V1, thEvStrictTrans1;

then ( w1 < wr2 & wr2 < e1 ) by ORDERS_2:def 6;

then wr2 in (w1,e1) interval_in (p2,tr) by H2;

hence contradiction by V1, H1; :: thesis: verum

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; :: thesis: verum

proof

M20:
r1 << e1
by V1, A0, thEvStrictPrec;
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r1w = the True of Values & Values is consistent )
by V2;
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 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

hence contradiction by Y2; :: thesis: verum

( 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

proof

hence
contradiction
by thLinPreordEvents, RR1; :: thesis: verum
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 )

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

( 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;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

D2:
r2 reads flag2, the False of Values
not r1 reads flag1, the False of Values

end;proof

hence
( r1 in tr & r1 reads turn, the True of Values )
by V1; :: thesis: verum
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r2w = the True of Values & Values is consistent )
by V2;
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 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

hence contradiction by Y2; :: thesis: verum

proof

DS is consistent
;
not r2 reads turn, the False of Values

end;proof

hence
r2 reads flag2, the False of Values
by V2; :: thesis: verum
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

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;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

( r2w << r1 & r1 <= e1 )
by ORDERS_2:def 6, Y2, V1;
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;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

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

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

M1:
wr2 << r2
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;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

proof

Q0:
( not u1 <= r2 or not r2 <= e1 )
r1 << e2
by V1, A0, thEvStrictPrec, A0s, thEvStrictTrans2;

then J1: wr2 << e2 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r2 << wr2

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; :: thesis: verum

end;then J1: wr2 << e2 by ORDERS_2:def 6, H1, thEvStrictTrans1;

J2: not r2 << wr2

proof

DS is consistent
;
assume
r2 << wr2
; :: thesis: contradiction

then ( w2 << wr2 & wr2 < e2 ) by ORDERS_2:def 6, J1, V2, thEvStrictTrans1;

then ( w2 < wr2 & wr2 < e2 ) by ORDERS_2:def 6;

then wr2 in (w2,e2) interval_in (p1,tr) by H2;

hence contradiction by V2, H1; :: thesis: verum

end;then ( w2 << wr2 & wr2 < e2 ) by ORDERS_2:def 6, J1, V2, thEvStrictTrans1;

then ( w2 < wr2 & wr2 < e2 ) by ORDERS_2:def 6;

then wr2 in (w2,e2) interval_in (p1,tr) by H2;

hence contradiction by V2, H1; :: thesis: verum

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; :: thesis: verum

proof

M20:
r2 << e1
by V2, A0s, A0, thEvStrictPrec, thEvStrictTrans2;
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

hence contradiction by Y2; :: thesis: verum

end;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

then
( val r1w = the True of Values & Values is consistent )
by V1;
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 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

hence contradiction by Y2; :: thesis: verum

( 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