{} 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₁( 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₁(p) from FUNCT_2:sch 4();
deffunc H₂( 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₂(tr) from FUNCT_2:sch 4();
deffunc H₃( 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₃(x) from FUNCT_2:sch 4();
deffunc H₄( 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₄(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

proof

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;

C2: Se is pr-ordered

proof

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;

C3: Se is rw-ordered

proof

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;

C4: Se is rw-consistent

proof

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;

Se is rw-exclusive

proof

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;

hence Se is consistent by C1, C2, C3, C4; :: thesis: verum