let P be set ; for N being Petri_net of P
for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
let N be Petri_net of P; for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
let e1, e2 be Element of N; {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
set C1 = <*e1*>;
set C2 = <*e2*>;
set R1 = {<*e1*>};
set R2 = {<*e2*>};
thus
{<*e1*>} concur {<*e2*>} c= {<*e1,e2*>,<*e2,e1*>}
XBOOLE_0:def 10 {<*e1,e2*>,<*e2,e1*>} c= {<*e1*>} concur {<*e2*>}proof
let x be
object ;
TARSKI:def 3 ( not x in {<*e1*>} concur {<*e2*>} or x in {<*e1,e2*>,<*e2,e1*>} )
assume
x in {<*e1*>} concur {<*e2*>}
;
x in {<*e1,e2*>,<*e2,e1*>}
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 {<*e1*>} &
Seq q2 in {<*e2*>} )
;
consider q1,
q2 being
FinSubsequence such that A3:
C = q1 \/ q2
and A4:
q1 misses q2
and A5:
Seq q1 in {<*e1*>}
and A6:
Seq q2 in {<*e2*>}
by A2;
A7:
Seq q1 = <*e1*>
by A5, TARSKI:def 1;
A8:
Seq q2 = <*e2*>
by A6, TARSKI:def 1;
consider i being
Element of
NAT such that A9:
q1 = {[i,e1]}
by A7, FINSEQ_3:159;
consider j being
Element of
NAT such that A10:
q2 = {[j,e2]}
by A8, FINSEQ_3:159;
A11:
[i,e1] in q1
by A9, TARSKI:def 1;
A12:
[j,e2] in q2
by A10, TARSKI:def 1;
A13:
C = {[i,e1],[j,e2]}
by A3, A9, A10, ENUMSET1:1;
then
( (
i = 1 &
j = 1 &
e1 = e2 ) or (
i = 1 &
j = 2 ) or (
i = 2 &
j = 1 ) )
by FINSEQ_1:98;
then
(
C = <*e1,e2*> or
C = <*e2,e1*> )
by A4, A11, A12, A13, FINSEQ_1:99, XBOOLE_0:3;
hence
x in {<*e1,e2*>,<*e2,e1*>}
by A1, TARSKI:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {<*e1,e2*>,<*e2,e1*>} or x in {<*e1*>} concur {<*e2*>} )
assume A14:
x in {<*e1,e2*>,<*e2,e1*>}
; x in {<*e1*>} concur {<*e2*>}
per cases
( x = <*e1,e2*> or x = <*e2,e1*> )
by A14, TARSKI:def 2;
suppose A15:
x = <*e1,e2*>
;
x in {<*e1*>} concur {<*e2*>}then A16:
x =
{[1,e1],[2,e2]}
by FINSEQ_1:99
.=
{[1,e1]} \/ {[2,e2]}
by ENUMSET1:1
;
reconsider q1 =
{[1,e1]},
q2 =
{[2,e2]} as
FinSubsequence by FINSEQ_1:96;
[1,e1] <> [2,e2]
by XTUPLE_0:1;
then
not
[1,e1] in q2
by TARSKI:def 1;
then A17:
q1 misses q2
by ZFMISC_1:50;
A18:
Seq q1 = <*e1*>
by FINSEQ_3:157;
A19:
Seq q2 = <*e2*>
by FINSEQ_3:157;
A20:
<*e1*> in {<*e1*>}
by TARSKI:def 1;
<*e2*> in {<*e2*>}
by TARSKI:def 1;
hence
x in {<*e1*>} concur {<*e2*>}
by A15, A16, A17, A18, A19, A20;
verum end; suppose A21:
x = <*e2,e1*>
;
x in {<*e1*>} concur {<*e2*>}then A22:
x =
{[1,e2],[2,e1]}
by FINSEQ_1:99
.=
{[1,e2]} \/ {[2,e1]}
by ENUMSET1:1
;
reconsider q1 =
{[2,e1]},
q2 =
{[1,e2]} as
FinSubsequence by FINSEQ_1:96;
[1,e2] <> [2,e1]
by XTUPLE_0:1;
then
not
[2,e1] in q2
by TARSKI:def 1;
then A23:
q1 misses q2
by ZFMISC_1:50;
A24:
Seq q1 = <*e1*>
by FINSEQ_3:157;
A25:
Seq q2 = <*e2*>
by FINSEQ_3:157;
A26:
<*e1*> in {<*e1*>}
by TARSKI:def 1;
<*e2*> in {<*e2*>}
by TARSKI:def 1;
hence
x in {<*e1*>} concur {<*e2*>}
by A21, A22, A23, A24, A25, A26;
verum end;