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

for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

let N be Petri_net of P; :: thesis: for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

let R1, R2 be process of N; :: thesis: R1 before R2 c= R1 concur R2

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

assume A1: x in R1 before R2 ; :: thesis: x in R1 concur R2

then reconsider C = x as firing-sequence of N ;

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

A2: x = C1 ^ C2 and

A3: C1 in R1 and

A4: C2 in R2 by A1;

set q1 = C1;

set q2 = (len C1) Shift C2;

reconsider q1 = C1 as FinSequence ;

A5: C = q1 \/ ((len C1) Shift C2) by A2, VALUED_1:49;

A6: q1 misses (len C1) Shift C2 by VALUED_1:50;

A7: Seq q1 in R1 by A3, FINSEQ_3:116;

Seq ((len C1) Shift C2) in R2 by A4, VALUED_1:46;

hence x in R1 concur R2 by A5, A6, A7; :: thesis: verum

for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

let N be Petri_net of P; :: thesis: for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

let R1, R2 be process of N; :: thesis: R1 before R2 c= R1 concur R2

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

assume A1: x in R1 before R2 ; :: thesis: x in R1 concur R2

then reconsider C = x as firing-sequence of N ;

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

A2: x = C1 ^ C2 and

A3: C1 in R1 and

A4: C2 in R2 by A1;

set q1 = C1;

set q2 = (len C1) Shift C2;

reconsider q1 = C1 as FinSequence ;

A5: C = q1 \/ ((len C1) Shift C2) by A2, VALUED_1:49;

A6: q1 misses (len C1) Shift C2 by VALUED_1:50;

A7: Seq q1 in R1 by A3, FINSEQ_3:116;

Seq ((len C1) Shift C2) in R2 by A4, VALUED_1:46;

hence x in R1 concur R2 by A5, A6, A7; :: thesis: verum