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

for R being process of N holds (NeutralProcess N) concur R = R

let N be Petri_net of P; :: thesis: for R being process of N holds (NeutralProcess N) concur R = R

let R be process of N; :: thesis: (NeutralProcess N) concur R = R

thus (NeutralProcess N) concur R c= R :: according to XBOOLE_0:def 10 :: thesis: R c= (NeutralProcess N) concur R

assume A6: x in R ; :: thesis: x in (NeutralProcess N) concur R

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

reconsider q1 = <*> N, q2 = C as FinSubsequence ;

A7: Seq q2 = C by FINSEQ_3:116;

A8: {} \/ q2 = C ;

A9: Seq q1 = q1 by FINSEQ_3:116;

A10: q1 in {(<*> N)} by TARSKI:def 1;

q1 misses q2 ;

hence x in (NeutralProcess N) concur R by A6, A7, A8, A9, A10; :: thesis: verum

for R being process of N holds (NeutralProcess N) concur R = R

let N be Petri_net of P; :: thesis: for R being process of N holds (NeutralProcess N) concur R = R

let R be process of N; :: thesis: (NeutralProcess N) concur R = R

thus (NeutralProcess N) concur R c= R :: according to XBOOLE_0:def 10 :: thesis: R c= (NeutralProcess N) concur R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in (NeutralProcess N) concur R )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (NeutralProcess N) concur R or x in R )

assume x in (NeutralProcess N) concur R ; :: thesis: x in 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 {(<*> N)} & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A3: C = q1 \/ q2 and

q1 misses q2 and

A4: Seq q1 in {(<*> N)} and

A5: Seq q2 in R by A2;

Seq q1 = {} by A4, TARSKI:def 1;

then q1 = {} by FINSEQ_1:97;

hence x in R by A1, A3, A5, FINSEQ_3:116; :: thesis: verum

end;assume x in (NeutralProcess N) concur R ; :: thesis: x in 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 {(<*> N)} & Seq q2 in R ) ;

consider q1, q2 being FinSubsequence such that

A3: C = q1 \/ q2 and

q1 misses q2 and

A4: Seq q1 in {(<*> N)} and

A5: Seq q2 in R by A2;

Seq q1 = {} by A4, TARSKI:def 1;

then q1 = {} by FINSEQ_1:97;

hence x in R by A1, A3, A5, FINSEQ_3:116; :: thesis: verum

assume A6: x in R ; :: thesis: x in (NeutralProcess N) concur R

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

reconsider q1 = <*> N, q2 = C as FinSubsequence ;

A7: Seq q2 = C by FINSEQ_3:116;

A8: {} \/ q2 = C ;

A9: Seq q1 = q1 by FINSEQ_3:116;

A10: q1 in {(<*> N)} by TARSKI:def 1;

q1 misses q2 ;

hence x in (NeutralProcess N) concur R by A6, A7, A8, A9, A10; :: thesis: verum