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
proof
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;
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 )
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;
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;
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;
end;