let P be set ; :: thesis: for N being Petri_net of P
for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
let N be Petri_net of P; :: thesis: for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
let R, R1, R2 be process of N; :: thesis: (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
thus (R1 \/ R2) before R c= (R1 before R) \/ (R2 before R) :: according to XBOOLE_0:def 10 :: thesis: (R1 before R) \/ (R2 before R) c= (R1 \/ R2) before R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 \/ R2) before R or x in (R1 before R) \/ (R2 before R) )
assume x in (R1 \/ R2) before R ; :: thesis: x in (R1 before R) \/ (R2 before R)
then consider fs1, fs being firing-sequence of N such that
A1: x = fs1 ^ fs and
A2: fs1 in R1 \/ R2 and
A3: fs in R ;
( fs1 in R1 or fs1 in R2 ) by A2, XBOOLE_0:def 3;
then ( x in { (a1 ^ a) where a1, a is firing-sequence of N : ( a1 in R1 & a in R ) } or x in { (b2 ^ b) where b2, b is firing-sequence of N : ( b2 in R2 & b in R ) } ) by A1, A3;
hence x in (R1 before R) \/ (R2 before R) by XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 before R) \/ (R2 before R) or x in (R1 \/ R2) before R )
assume A4: x in (R1 before R) \/ (R2 before R) ; :: thesis: x in (R1 \/ R2) before R
per cases ( x in R1 before R or x in R2 before R ) by A4, XBOOLE_0:def 3;
suppose x in R1 before R ; :: thesis: x in (R1 \/ R2) before R
then consider fs1, fs being firing-sequence of N such that
A5: x = fs1 ^ fs and
A6: fs1 in R1 and
A7: fs in R ;
fs1 in R1 \/ R2 by A6, XBOOLE_0:def 3;
hence x in (R1 \/ R2) before R by A5, A7; :: thesis: verum
end;
suppose x in R2 before R ; :: thesis: x in (R1 \/ R2) before R
then consider fs2, fs being firing-sequence of N such that
A8: x = fs2 ^ fs and
A9: fs2 in R2 and
A10: fs in R ;
fs2 in R1 \/ R2 by A9, XBOOLE_0:def 3;
hence x in (R1 \/ R2) before R by A8, A10; :: thesis: verum
end;
end;