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;
A32: now :: thesis: for x being set holds
( not x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) or x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 )
let x be set ; :: thesis: ( not x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) or x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 )
assume x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) ; :: thesis: ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 )
then ( x in dom (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) or x in dom q21 ) by FUNCT_4:12;
then ( x in dom ( the firing-rule of CPNT1 +* the firing-rule of CPNT2) or x in dom q12 or x in dom q21 ) by FUNCT_4:12;
hence ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 ) by FUNCT_4:12; :: thesis: verum
end;
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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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)) ; :: thesis: verum
end;
suppose A37: t in dom the firing-rule of CPNT2 ; :: thesis: 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)) ; :: thesis: verum
end;
suppose A39: t in dom q12 ; :: thesis: 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} *'
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Im (O12,t1) or x in {t} *' )
A40: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
assume A41: x in Im (O12,t1) ; :: thesis: x in {t} *'
then reconsider s = x as place of CPNT2 ;
A42: [t1,s] in O12 by A41, RELSET_2:9;
O12 c= E31 \/ E32 by XBOOLE_1:7;
then O12 c= the T-S_Arcs of CPNT12 by A40;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A42;
A43: the carrier of CPNT2 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A44: f = [t,s] ;
A45: t in {t} by TARSKI:def 1;
s in the carrier of CPNT2 ;
hence x in {t} *' by A43, A45, A44; :: thesis: verum
end;
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)) ; :: thesis: verum
end;
suppose A46: t in dom q21 ; :: thesis: 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} *'
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Im (O21,t1) or x in {t} *' )
A47: O21 c= E31 \/ E32 by XBOOLE_1:7;
assume A48: x in Im (O21,t1) ; :: thesis: x in {t} *'
then reconsider s = x as place of CPNT1 ;
A49: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
[t1,s] in O21 by A48, RELSET_2:9;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A47, A49;
A50: the carrier of CPNT1 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A51: f = [t,s] ;
A52: t in {t} by TARSKI:def 1;
s in the carrier of CPNT1 ;
hence x in {t} *' by A50, A52, A51; :: thesis: 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, 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)) ; :: thesis: verum
end;
end;
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)) ; :: thesis: verum
end;
A53: TS12 = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 by XBOOLE_1:4;
A54: now :: thesis: for x being object st x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) holds
x in the carrier' of CPNT1 \/ the carrier' of CPNT2
let x be object ; :: thesis: ( x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) implies x in the carrier' of CPNT1 \/ the carrier' of CPNT2 )
dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (Outbds CPNT1) by Def11;
then A55: dom the firing-rule of CPNT1 c= the carrier' of CPNT1 by XBOOLE_1:1;
dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (Outbds CPNT2) by Def11;
then A56: dom the firing-rule of CPNT2 c= the carrier' of CPNT2 by XBOOLE_1:1;
assume x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) ; :: thesis: x in the carrier' of CPNT1 \/ the carrier' of CPNT2
then ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 ) by A32;
hence x in the carrier' of CPNT1 \/ the carrier' of CPNT2 by A9, A10, A55, A56, XBOOLE_0:def 3; :: thesis: verum
end;
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)
proof
set RR4 = q21;
set RR3 = q12;
set RR2 = the firing-rule of CPNT2;
set RR1 = the firing-rule of CPNT1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the firing-rule of CPNT12 or x in the carrier' of CPNT12 \ (Outbds CPNT12) )
assume A58: x in dom the firing-rule of CPNT12 ; :: thesis: x in the carrier' of CPNT12 \ (Outbds CPNT12)
then reconsider t = x as transition of CPNT12 by A54;
now :: thesis: not x in Outbds CPNT12
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, A58;
suppose A59: t in dom the firing-rule of CPNT1 ; :: thesis: not x in Outbds CPNT12
A60: dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (Outbds CPNT1) by Def11;
then reconsider t1 = t as transition of CPNT1 by A59, XBOOLE_0:def 5;
not t in Outbds CPNT1 by A59, A60, XBOOLE_0:def 5;
then not t1 is outbound ;
then {t1} *' <> {} ;
then A61: ex g being object st g in {t1} *' by XBOOLE_0:def 1;
{t1} *' c= {t} *' by A26, A27, A28, Th7;
then for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by A61;
hence not x in Outbds CPNT12 ; :: thesis: verum
end;
suppose A62: t in dom the firing-rule of CPNT2 ; :: thesis: not x in Outbds CPNT12
A63: dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (Outbds CPNT2) by Def11;
then reconsider t1 = t as transition of CPNT2 by A62, XBOOLE_0:def 5;
not t in Outbds CPNT2 by A62, A63, XBOOLE_0:def 5;
then not t1 is outbound ;
then {t1} *' <> {} ;
then A64: ex g being object st g in {t1} *' by XBOOLE_0:def 1;
{t1} *' c= {t} *' by A29, A31, A30, Th7;
then for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by A64;
hence not x in Outbds CPNT12 ; :: thesis: verum
end;
suppose t in dom q12 ; :: thesis: not x in Outbds CPNT12
then t in dom O12 by A9, FUNCT_2:def 1;
then consider s being object such that
A65: [t,s] in O12 by XTUPLE_0:def 12;
reconsider s = s as place of CPNT2 by A65, ZFMISC_1:87;
A66: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
O12 c= E31 \/ E32 by XBOOLE_1:7;
then O12 c= the T-S_Arcs of CPNT12 by A66;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A65;
A67: the carrier of CPNT2 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A68: f = [t,s] ;
A69: t in {t} by TARSKI:def 1;
s in the carrier of CPNT2 ;
then s in {t} *' by A67, A69, A68;
then for w being transition of CPNT12 holds
( not t = w or not w is outbound ) ;
hence not x in Outbds CPNT12 ; :: thesis: verum
end;
suppose t in dom q21 ; :: thesis: not x in Outbds CPNT12
then t in dom O21 by A10, FUNCT_2:def 1;
then consider s being object such that
A70: [t,s] in O21 by XTUPLE_0:def 12;
reconsider s = s as place of CPNT1 by A70, ZFMISC_1:87;
A71: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
O21 c= E31 \/ E32 by XBOOLE_1:7;
then O21 c= the T-S_Arcs of CPNT12 by A71;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A70;
A72: the carrier of CPNT1 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A73: f = [t,s] ;
A74: t in {t} by TARSKI:def 1;
s in the carrier of CPNT1 ;
then s in {t} *' by A72, A74, A73;
then for w being transition of CPNT12 holds
( not t = w or not w is outbound ) ;
hence not x in Outbds CPNT12 ; :: thesis: verum
end;
end;
end;
hence x in the carrier' of CPNT12 \ (Outbds CPNT12) by A57, A58, XBOOLE_0:def 5; :: thesis: verum
end;
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; :: thesis: verum