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

for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

let N be Petri_net of P; :: thesis: for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

let R, R1, R2 be process of N; :: thesis: (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

thus (R1 \/ R2) concur R c= (R1 concur R) \/ (R2 concur R) :: according to XBOOLE_0:def 10 :: thesis: (R1 concur R) \/ (R2 concur R) c= (R1 \/ R2) concur R

assume A7: x in (R1 concur R) \/ (R2 concur R) ; :: thesis: x in (R1 \/ R2) concur R

for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

let N be Petri_net of P; :: thesis: for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

let R, R1, R2 be process of N; :: thesis: (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

thus (R1 \/ R2) concur R c= (R1 concur R) \/ (R2 concur R) :: according to XBOOLE_0:def 10 :: thesis: (R1 concur R) \/ (R2 concur R) c= (R1 \/ R2) concur R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R) \/ (R2 concur R) or x in (R1 \/ R2) concur R )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 \/ R2) concur R or x in (R1 concur R) \/ (R2 concur R) )

assume x in (R1 \/ R2) concur R ; :: thesis: x in (R1 concur R) \/ (R2 concur R)

then consider C being firing-sequence of N such that

A1: x = C and

A2: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A3: C = q1 \/ q2 and

A4: q1 misses q2 and

A5: Seq q1 in R1 \/ R2 and

A6: Seq q2 in R by A2;

( Seq q1 in R1 or Seq q1 in R2 ) by A5, XBOOLE_0:def 3;

then ( x in { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) } or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) } ) by A1, A3, A4, A6;

hence x in (R1 concur R) \/ (R2 concur R) by XBOOLE_0:def 3; :: thesis: verum

end;assume x in (R1 \/ R2) concur R ; :: thesis: x in (R1 concur R) \/ (R2 concur R)

then consider C being firing-sequence of N such that

A1: x = C and

A2: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A3: C = q1 \/ q2 and

A4: q1 misses q2 and

A5: Seq q1 in R1 \/ R2 and

A6: Seq q2 in R by A2;

( Seq q1 in R1 or Seq q1 in R2 ) by A5, XBOOLE_0:def 3;

then ( x in { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) } or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) } ) by A1, A3, A4, A6;

hence x in (R1 concur R) \/ (R2 concur R) by XBOOLE_0:def 3; :: thesis: verum

assume A7: x in (R1 concur R) \/ (R2 concur R) ; :: thesis: x in (R1 \/ R2) concur R

per cases
( x in R1 concur R or x in R2 concur R )
by A7, XBOOLE_0:def 3;

end;

suppose
x in R1 concur R
; :: thesis: x in (R1 \/ R2) concur R

then consider C being firing-sequence of N such that

A8: x = C and

A9: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A10: C = q1 \/ q2 and

A11: q1 misses q2 and

A12: Seq q1 in R1 and

A13: Seq q2 in R by A9;

Seq q1 in R1 \/ R2 by A12, XBOOLE_0:def 3;

hence x in (R1 \/ R2) concur R by A8, A10, A11, A13; :: thesis: verum

end;A8: x = C and

A9: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A10: C = q1 \/ q2 and

A11: q1 misses q2 and

A12: Seq q1 in R1 and

A13: Seq q2 in R by A9;

Seq q1 in R1 \/ R2 by A12, XBOOLE_0:def 3;

hence x in (R1 \/ R2) concur R by A8, A10, A11, A13; :: thesis: verum

suppose
x in R2 concur R
; :: thesis: x in (R1 \/ R2) concur R

then consider C being firing-sequence of N such that

A14: x = C and

A15: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A16: C = q1 \/ q2 and

A17: q1 misses q2 and

A18: Seq q1 in R2 and

A19: Seq q2 in R by A15;

Seq q1 in R1 \/ R2 by A18, XBOOLE_0:def 3;

hence x in (R1 \/ R2) concur R by A14, A16, A17, A19; :: thesis: verum

end;A14: x = C and

A15: ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A16: C = q1 \/ q2 and

A17: q1 misses q2 and

A18: Seq q1 in R2 and

A19: Seq q2 in R by A15;

Seq q1 in R1 \/ R2 by A18, XBOOLE_0:def 3;

hence x in (R1 \/ R2) concur R by A14, A16, A17, A19; :: thesis: verum