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:7;
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:7;
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:7;
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:7;
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 Def14;
A14:
dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (dom q21)
by A10, Def11;
the carrier' of CPNT2 c= T12
by XBOOLE_1:7;
then A15:
Outbds CPNT2 c= T12
;
the carrier' of CPNT1 c= T12
by XBOOLE_1:7;
then A16:
Outbds CPNT1 c= T12
;
A17:
the carrier' of CPNT1 /\ the carrier' of CPNT2 = {}
by A1;
A18:
dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (dom q12)
by A9, Def11;
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:7;
the carrier of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E31 = O12 as Relation of T12,P12 by A16, RELSET_1:7;
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) #);
A25:
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
;
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
;
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 A25;
A26:
the carrier of CPNT1 c= the carrier of CPNT12
by XBOOLE_1:7;
A27:
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 A28:
the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12
by A6;
A29:
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 A30:
the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
by A7;
A31:
the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12
by XBOOLE_1:7;
A33:
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 A34:
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 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))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 A32, A34;
suppose A35:
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 Def11;
then reconsider t1 =
t as
transition of
CPNT1 by A35, 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 A36:
the
firing-rule of
CPNT1 . t1 is
Function of
(thin_cylinders (CS1,I1)),
(thin_cylinders (CS1,O1))
by A35, Def11;
*' {t1} c= *' {t}
by A26, A27, A28, 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 A26, A27, A28, 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, A35, A36, 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 A37:
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 Def11;
then reconsider t1 =
t as
transition of
CPNT2 by A37, 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 A38:
the
firing-rule of
CPNT2 . t1 is
Function of
(thin_cylinders (CS1,I1)),
(thin_cylinders (CS1,O1))
by A37, Def11;
*' {t1} c= *' {t}
by A29, A31, A30, 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 A29, A31, A30, 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, A37, 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 A39:
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 A26, A27, A28, 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, A39;
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, A39, 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 A46:
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 A29, A31, A30, 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} *'
then reconsider O =
Im (
O21,
t1) as
Subset of
({t} *') ;
ex
x1 being
transition of
CPNT2 st
(
t1 = x1 &
x1 is
outbound )
by A10, A46;
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, A46, 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;
A53:
TS12 = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21
by XBOOLE_1:4;
then A57:
dom the firing-rule of CPNT12 c= the carrier' of CPNT12
;
dom the firing-rule of CPNT12 c= the carrier' of CPNT12 \ (Outbds CPNT12)
then
CPNT12 is Colored-PT-net-like
by A33;
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, A53; verum