let P be set ; :: thesis: for N being Petri_net of P

for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

let N be Petri_net of P; :: thesis: for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

let R1, R2, R3 be process of N; :: thesis: (R1 before R2) before R3 = R1 before (R2 before R3)

thus (R1 before R2) before R3 c= R1 before (R2 before R3) :: according to XBOOLE_0:def 10 :: thesis: R1 before (R2 before R3) c= (R1 before R2) before R3

assume x in R1 before (R2 before R3) ; :: thesis: x in (R1 before R2) before R3

then consider C1, C2 being firing-sequence of N such that

A11: x = C1 ^ C2 and

A12: C1 in R1 and

A13: C2 in R2 before R3 ;

consider fs1, fs2 being firing-sequence of N such that

A14: C2 = fs1 ^ fs2 and

A15: fs1 in R2 and

A16: fs2 in R3 by A13;

A17: x = (C1 ^ fs1) ^ fs2 by A11, A14, FINSEQ_1:32;

consider C being firing-sequence of N such that

A18: C = C1 ^ fs1 and

A19: C1 in R1 and

A20: fs1 in R2 by A12, A15;

C in R1 before R2 by A18, A19, A20;

hence x in (R1 before R2) before R3 by A16, A17, A18; :: thesis: verum

for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

let N be Petri_net of P; :: thesis: for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

let R1, R2, R3 be process of N; :: thesis: (R1 before R2) before R3 = R1 before (R2 before R3)

thus (R1 before R2) before R3 c= R1 before (R2 before R3) :: according to XBOOLE_0:def 10 :: thesis: R1 before (R2 before R3) c= (R1 before R2) before R3

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 before (R2 before R3) or x in (R1 before R2) before R3 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 before R2) before R3 or x in R1 before (R2 before R3) )

assume x in (R1 before R2) before R3 ; :: thesis: x in R1 before (R2 before R3)

then consider C1, C2 being firing-sequence of N such that

A1: x = C1 ^ C2 and

A2: C1 in R1 before R2 and

A3: C2 in R3 ;

consider fs1, fs2 being firing-sequence of N such that

A4: C1 = fs1 ^ fs2 and

A5: fs1 in R1 and

A6: fs2 in R2 by A2;

A7: x = fs1 ^ (fs2 ^ C2) by A1, A4, FINSEQ_1:32;

consider C3 being firing-sequence of N such that

A8: C3 = fs2 ^ C2 and

A9: fs2 in R2 and

A10: C2 in R3 by A3, A6;

C3 in R2 before R3 by A8, A9, A10;

hence x in R1 before (R2 before R3) by A5, A7, A8; :: thesis: verum

end;assume x in (R1 before R2) before R3 ; :: thesis: x in R1 before (R2 before R3)

then consider C1, C2 being firing-sequence of N such that

A1: x = C1 ^ C2 and

A2: C1 in R1 before R2 and

A3: C2 in R3 ;

consider fs1, fs2 being firing-sequence of N such that

A4: C1 = fs1 ^ fs2 and

A5: fs1 in R1 and

A6: fs2 in R2 by A2;

A7: x = fs1 ^ (fs2 ^ C2) by A1, A4, FINSEQ_1:32;

consider C3 being firing-sequence of N such that

A8: C3 = fs2 ^ C2 and

A9: fs2 in R2 and

A10: C2 in R3 by A3, A6;

C3 in R2 before R3 by A8, A9, A10;

hence x in R1 before (R2 before R3) by A5, A7, A8; :: thesis: verum

assume x in R1 before (R2 before R3) ; :: thesis: x in (R1 before R2) before R3

then consider C1, C2 being firing-sequence of N such that

A11: x = C1 ^ C2 and

A12: C1 in R1 and

A13: C2 in R2 before R3 ;

consider fs1, fs2 being firing-sequence of N such that

A14: C2 = fs1 ^ fs2 and

A15: fs1 in R2 and

A16: fs2 in R3 by A13;

A17: x = (C1 ^ fs1) ^ fs2 by A11, A14, FINSEQ_1:32;

consider C being firing-sequence of N such that

A18: C = C1 ^ fs1 and

A19: C1 in R1 and

A20: fs1 in R2 by A12, A15;

C in R1 before R2 by A18, A19, A20;

hence x in (R1 before R2) before R3 by A16, A17, A18; :: thesis: verum