{} 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 H1( 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 = H1(p) from deffunc H2( 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 = H2(tr) from deffunc H3( 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 = H3(x) from deffunc H4( 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 = H4(x) from 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: thesis: verum
end;
hence Se is consistent by C1, C2, C3, C4; :: thesis: verum