{} is Element of bool the carrier of the non empty LinearPreorder
by SUBSET_1:1;

then consider E0 being Element of bool the carrier of the non empty LinearPreorder such that

E0def: E0 = {} ;

deffunc H_{1}( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;

consider procE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

procE0def: for p being Element of the non empty set holds procE0 . p = H_{1}(p)
from FUNCT_2:sch 4();

deffunc H_{2}( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;

consider traceE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

traceE0def: for tr being Element of the non empty set holds traceE0 . tr = H_{2}(tr)
from FUNCT_2:sch 4();

deffunc H_{3}( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;

consider readE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

readE0def: for x being Element of the non empty set holds readE0 . x = H_{3}(x)
from FUNCT_2:sch 4();

deffunc H_{4}( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;

consider writeE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

writeE0def: for x being Element of the non empty set holds writeE0 . x = H_{4}(x)
from FUNCT_2:sch 4();

take Se = Events_structure(# the non empty LinearPreorder, the non empty set , the non empty set , the non empty set ,procE0,traceE0,readE0,writeE0, the PartFunc of the carrier of the non empty LinearPreorder, the carrier of Values #); :: thesis: Se is consistent

C1: Se is pr-complete

then consider E0 being Element of bool the carrier of the non empty LinearPreorder such that

E0def: E0 = {} ;

deffunc H

consider procE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

procE0def: for p being Element of the non empty set holds procE0 . p = H

deffunc H

consider traceE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

traceE0def: for tr being Element of the non empty set holds traceE0 . tr = H

deffunc H

consider readE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

readE0def: for x being Element of the non empty set holds readE0 . x = H

deffunc H

consider writeE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that

writeE0def: for x being Element of the non empty set holds writeE0 . x = H

take Se = Events_structure(# the non empty LinearPreorder, the non empty set , the non empty set , the non empty set ,procE0,traceE0,readE0,writeE0, the PartFunc of the carrier of the non empty LinearPreorder, the carrier of Values #); :: thesis: Se is consistent

C1: Se is pr-complete

proof

C2:
Se is pr-ordered
let tr be trace of Se; :: according to PETERSON:def 13 :: thesis: for e being Event of Se st e in tr holds

ex p being Process of Se st e in p

let e be Event of Se; :: thesis: ( e in tr implies ex p being Process of Se st e in p )

assume U1: e in tr ; :: thesis: ex p being Process of Se st e in p

take the Process of Se ; :: thesis: e in the Process of Se

thus e in the Process of Se by U1, E0def, traceE0def; :: thesis: verum

end;ex p being Process of Se st e in p

let e be Event of Se; :: thesis: ( e in tr implies ex p being Process of Se st e in p )

assume U1: e in tr ; :: thesis: ex p being Process of Se st e in p

take the Process of Se ; :: thesis: e in the Process of Se

thus e in the Process of Se by U1, E0def, traceE0def; :: thesis: verum

proof

C3:
Se is rw-ordered
let p be Process of Se; :: according to PETERSON:def 14 :: thesis: for e1, e2 being Event of Se st e1 in p & e2 in p & e1 <= e2 & e2 <= e1 holds

e1 = e2

let e1, e2 be Event of Se; :: thesis: ( e1 in p & e2 in p & e1 <= e2 & e2 <= e1 implies e1 = e2 )

assume U1: ( e1 in p & e2 in p ) ; :: thesis: ( not e1 <= e2 or not e2 <= e1 or e1 = e2 )

thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, procE0def; :: thesis: verum

end;e1 = e2

let e1, e2 be Event of Se; :: thesis: ( e1 in p & e2 in p & e1 <= e2 & e2 <= e1 implies e1 = e2 )

assume U1: ( e1 in p & e2 in p ) ; :: thesis: ( not e1 <= e2 or not e2 <= e1 or e1 = e2 )

thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, procE0def; :: thesis: verum

proof

C4:
Se is rw-consistent
let x be Location of Se; :: according to PETERSON:def 15 :: thesis: for e1, e2 being Event of Se st ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 holds

e1 = e2

let e1, e2 be Event of Se; :: thesis: ( ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 implies e1 = e2 )

assume U1: ( ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) ) ; :: thesis: ( not e1 <= e2 or not e2 <= e1 or e1 = e2 )

thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, readE0def, writeE0def; :: thesis: verum

end;e1 = e2

let e1, e2 be Event of Se; :: thesis: ( ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) & e1 <= e2 & e2 <= e1 implies e1 = e2 )

assume U1: ( ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) ) ; :: thesis: ( not e1 <= e2 or not e2 <= e1 or e1 = e2 )

thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, readE0def, writeE0def; :: thesis: verum

proof

Se is rw-exclusive
let tr be trace of Se; :: according to PETERSON:def 16 :: thesis: for x being Location of Se

for e being Event of Se

for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let x be Location of Se; :: thesis: for e being Event of Se

for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let e be Event of Se; :: thesis: for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let a be Element of the carrier of Values; :: thesis: ( e in tr & e reads x & val e = a implies ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) ) )

assume U1: ( e in tr & e reads x & val e = a ) ; :: thesis: ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

thus ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) ) by U1, E0def, traceE0def; :: thesis: verum

end;for e being Event of Se

for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let x be Location of Se; :: thesis: for e being Event of Se

for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let e be Event of Se; :: thesis: for a being Element of the carrier of Values st e in tr & e reads x & val e = a holds

ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

let a be Element of the carrier of Values; :: thesis: ( e in tr & e reads x & val e = a implies ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) ) )

assume U1: ( e in tr & e reads x & val e = a ) ; :: thesis: ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) )

thus ex e0 being Event of Se st

( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds

e1 <= e0 ) ) by U1, E0def, traceE0def; :: thesis: verum

proof

hence
Se is consistent
by C1, C2, C3, C4; :: thesis: verum
let e be Event of Se; :: according to PETERSON:def 17 :: thesis: for x1, x2 being Location of Se holds

( not e reads x1 or not e writesto x2 )

let x1, x2 be Location of Se; :: thesis: ( not e reads x1 or not e writesto x2 )

thus ( not e reads x1 or not e writesto x2 ) by E0def, readE0def; :: thesis: verum

end;( not e reads x1 or not e writesto x2 )

let x1, x2 be Location of Se; :: thesis: ( not e reads x1 or not e writesto x2 )

thus ( not e reads x1 or not e writesto x2 ) by E0def, readE0def; :: thesis: verum