reconsider CS12 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 as non empty finite set ;
reconsider T12 = the carrier' of CPNT1 \/ the carrier' of CPNT2 as non empty set ;
reconsider P12 = the carrier of CPNT1 \/ the carrier of CPNT2 as non empty set ;
A2:
the carrier' of CPNT1 c= T12
by XBOOLE_1:7;
the carrier of CPNT1 c= P12
by XBOOLE_1:7;
then reconsider E1 = the S-T_Arcs of CPNT1 as Relation of P12,T12 by A2, RELSET_1:17;
A3:
the carrier of CPNT2 c= P12
by XBOOLE_1:7;
the carrier' of CPNT2 c= T12
by XBOOLE_1:7;
then reconsider E22 = the T-S_Arcs of CPNT2 as Relation of T12,P12 by A3, RELSET_1:17;
set R1 = the firing-rule of CPNT1;
A4:
the carrier' of CPNT2 c= T12
by XBOOLE_1:7;
the carrier of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E2 = the S-T_Arcs of CPNT2 as Relation of P12,T12 by A4, RELSET_1:17;
set R2 = the firing-rule of CPNT2;
A5:
the carrier of CPNT1 c= P12
by XBOOLE_1:7;
the carrier' of CPNT1 c= T12
by XBOOLE_1:7;
then reconsider E21 = the T-S_Arcs of CPNT1 as Relation of T12,P12 by A5, RELSET_1:17;
A6:
the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
E1 \/ E2 is Relation of P12,T12
;
then reconsider ST12 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 as non empty Relation of P12,T12 ;
A7:
the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
E21 \/ E22 is Relation of T12,P12
;
then reconsider TTS12 = the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 as non empty Relation of T12,P12 ;
consider q12, q21 being Function, O12 being Function of (Outbds CPNT1),the carrier of CPNT2, O21 being Function of (Outbds CPNT2),the carrier of CPNT1 such that
A8:
O = [O12,O21]
and
A9:
dom q12 = Outbds CPNT1
and
A10:
dom q21 = Outbds CPNT2
and
A11:
for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01))
and
A12:
for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02))
and
A13:
q = [q12,q21]
by Def13;
A14:
dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (dom q21)
by A10, Def10;
the carrier' of CPNT2 c= T12
by XBOOLE_1:7;
then A15:
Outbds CPNT2 c= T12
by XBOOLE_1:1;
the carrier' of CPNT1 c= T12
by XBOOLE_1:7;
then A16:
Outbds CPNT1 c= T12
by XBOOLE_1:1;
A17:
the carrier' of CPNT1 /\ the carrier' of CPNT2 = {}
by A1, Def11;
A18:
dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (dom q12)
by A9, Def10;
then A19:
(dom the firing-rule of CPNT1) /\ (dom the firing-rule of CPNT2) = {}
by A9, A10, A17, A14, Lm6;
A20:
(dom the firing-rule of CPNT2) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A21:
(dom the firing-rule of CPNT2) /\ (dom q12) = {}
by A9, A10, A17, A18, A14, Lm6;
A22:
(dom q12) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A23:
(dom the firing-rule of CPNT1) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A24:
(dom the firing-rule of CPNT1) /\ (dom q12) = {}
by A9, A10, A17, A18, A14, Lm6;
the carrier of CPNT1 c= P12
by XBOOLE_1:7;
then reconsider E32 = O21 as Relation of T12,P12 by A15, RELSET_1:17;
the carrier of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E31 = O12 as Relation of T12,P12 by A16, RELSET_1:17;
set R4 = q21;
set R3 = q12;
set CR12 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21;
reconsider TS12 = TTS12 \/ (E31 \/ E32) as non empty Relation of T12,P12 ;
set CPNT12 = Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #);
A:
Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) is with_S-T_arc
by PETRI:def 1;
Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) is with_T-S_arc
by PETRI:def 2;
then reconsider CPNT12 = Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) as Colored_Petri_net by A;
A25:
the carrier of CPNT1 c= the carrier of CPNT12
by XBOOLE_1:7;
A26:
the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT12
by XBOOLE_1:7;
the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
by XBOOLE_1:7;
then A27:
the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12
by A6, XBOOLE_1:1;
A28:
the carrier of CPNT2 c= the carrier of CPNT12
by XBOOLE_1:7;
the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
by XBOOLE_1:7;
then A29:
the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
by A7, XBOOLE_1:1;
A30:
the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12
by XBOOLE_1:7;
A32:
for t being transition of CPNT12 st t in dom the firing-rule of CPNT12 holds
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)
proof
let t be
transition of
CPNT12;
( t in dom the firing-rule of CPNT12 implies ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O) )
assume A33:
t in dom the
firing-rule of
CPNT12
;
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)
now per cases
( t in dom the firing-rule of CPNT1 or t in dom the firing-rule of CPNT2 or t in dom q12 or t in dom q21 )
by A31, A33;
suppose A34:
t in dom the
firing-rule of
CPNT1
;
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)
dom the
firing-rule of
CPNT1 c= the
carrier' of
CPNT1 \ (Outbds CPNT1)
by Def10;
then reconsider t1 =
t as
transition of
CPNT1 by A34, TARSKI:def 3;
consider CS1 being non
empty Subset of the
ColoredSet of
CPNT1,
I1 being
Subset of
(*' {t1}),
O1 being
Subset of
({t1} *' ) such that A35:
the
firing-rule of
CPNT1 . t1 is
Function of
(thin_cylinders CS1,I1),
(thin_cylinders CS1,O1)
by A34, Def10;
*' {t1} c= *' {t}
by A25, A26, A27, Th7;
then reconsider I =
I1 as
Subset of
(*' {t}) by XBOOLE_1:1;
the
ColoredSet of
CPNT1 c= the
ColoredSet of
CPNT12
by XBOOLE_1:7;
then reconsider CS =
CS1 as non
empty Subset of the
ColoredSet of
CPNT12 by XBOOLE_1:1;
{t1} *' c= {t} *'
by A25, A26, A27, Th7;
then reconsider O =
O1 as
Subset of
({t} *' ) by XBOOLE_1:1;
the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
by A19, A24, A23, A21, A20, A22, A34, A35, Lm5;
hence
ex
CS being non
empty Subset of the
ColoredSet of
CPNT12 ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) st the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
;
verum end; suppose A36:
t in dom the
firing-rule of
CPNT2
;
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)
dom the
firing-rule of
CPNT2 c= the
carrier' of
CPNT2 \ (Outbds CPNT2)
by Def10;
then reconsider t1 =
t as
transition of
CPNT2 by A36, TARSKI:def 3;
consider CS1 being non
empty Subset of the
ColoredSet of
CPNT2,
I1 being
Subset of
(*' {t1}),
O1 being
Subset of
({t1} *' ) such that A37:
the
firing-rule of
CPNT2 . t1 is
Function of
(thin_cylinders CS1,I1),
(thin_cylinders CS1,O1)
by A36, Def10;
*' {t1} c= *' {t}
by A28, A30, A29, Th7;
then reconsider I =
I1 as
Subset of
(*' {t}) by XBOOLE_1:1;
the
ColoredSet of
CPNT2 c= the
ColoredSet of
CPNT12
by XBOOLE_1:7;
then reconsider CS =
CS1 as non
empty Subset of the
ColoredSet of
CPNT12 by XBOOLE_1:1;
{t1} *' c= {t} *'
by A28, A30, A29, Th7;
then reconsider O =
O1 as
Subset of
({t} *' ) by XBOOLE_1:1;
the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
by A19, A24, A23, A21, A20, A22, A36, A37, Lm5;
hence
ex
CS being non
empty Subset of the
ColoredSet of
CPNT12 ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) st the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
;
verum end; suppose A38:
t in dom q12
;
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)then reconsider t1 =
t as
transition of
CPNT1 by A9;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by A25, A26, A27, Th7;
reconsider CS = the
ColoredSet of
CPNT1 as non
empty Subset of the
ColoredSet of
CPNT12 by XBOOLE_1:7;
Im O12,
t1 c= {t} *'
then reconsider O =
Im O12,
t1 as
Subset of
({t} *' ) ;
ex
x1 being
transition of
CPNT1 st
(
t1 = x1 &
x1 is
outbound )
by A9, A38;
then
q12 . t1 is
Function of
(thin_cylinders the ColoredSet of CPNT1,(*' {t1})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t1))
by A11;
then
the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
by A19, A24, A23, A21, A20, A22, A38, Lm5;
hence
ex
CS being non
empty Subset of the
ColoredSet of
CPNT12 ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) st the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
;
verum end; suppose A45:
t in dom q21
;
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT12 . t is Function of (thin_cylinders CS,I),(thin_cylinders CS,O)then reconsider t1 =
t as
transition of
CPNT2 by A10;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by A28, A30, A29, Th7;
reconsider CS = the
ColoredSet of
CPNT2 as non
empty Subset of the
ColoredSet of
CPNT12 by XBOOLE_1:7;
Im O21,
t1 c= {t} *'
proof
let x be
set ;
TARSKI:def 3 ( not x in Im O21,t1 or x in {t} *' )
A46:
O21 c= E31 \/ E32
by XBOOLE_1:7;
assume A47:
x in Im O21,
t1
;
x in {t} *'
then reconsider s =
x as
place of
CPNT1 ;
A48:
E31 \/ E32 c= the
T-S_Arcs of
CPNT12
by XBOOLE_1:7;
[t1,s] in O21
by A47, RELSET_2:9;
then reconsider f =
[t,s] as
T-S_arc of
CPNT12 by A46, A48, TARSKI:def 3;
A49:
the
carrier of
CPNT1 c= the
carrier of
CPNT1 \/ the
carrier of
CPNT2
by XBOOLE_1:7;
A50:
f = [t,s]
;
A51:
t in {t}
by TARSKI:def 1;
s in the
carrier of
CPNT1
;
hence
x in {t} *'
by A49, A51, A50;
verum
end; then reconsider O =
Im O21,
t1 as
Subset of
({t} *' ) ;
ex
x1 being
transition of
CPNT2 st
(
t1 = x1 &
x1 is
outbound )
by A10, A45;
then
q21 . t1 is
Function of
(thin_cylinders the ColoredSet of CPNT2,(*' {t1})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t1))
by A12;
then
the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
by A19, A24, A23, A21, A20, A22, A45, Lm5;
hence
ex
CS being non
empty Subset of the
ColoredSet of
CPNT12 ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) st the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
;
verum end;
hence
ex
CS being non
empty Subset of the
ColoredSet of
CPNT12 ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) st the
firing-rule of
CPNT12 . t is
Function of
(thin_cylinders CS,I),
(thin_cylinders CS,O)
;
verum
end;
A52:
TS12 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21
by XBOOLE_1:4;
then A56:
dom the firing-rule of CPNT12 c= the carrier' of CPNT12
by TARSKI:def 3;
dom the firing-rule of CPNT12 c= the carrier' of CPNT12 \ (Outbds CPNT12)
then
CPNT12 is Colored-PT-net-like
by A32, Def10;
hence
ex b1 being strict Colored-PT-net ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1),the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2),the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) ) & q = [q12,q21] & the carrier of b1 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b1 = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b1 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b1 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b1 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b1 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 )
by A8, A9, A10, A11, A12, A13, A52; verum