let CA, CB be strict Colored-PT-net; :: thesis: ( 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 CA = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) & 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 CB = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) implies CA = CB )
assume ex q12A, q21A being Function ex O12A being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21A being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12A,O21A] & dom q12A = Outbds CPNT1 & dom q21A = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12A . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12A,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21A . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21A,t02)))) ) & q = [q12A,q21A] & the carrier of CA = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A & the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12A) +* q21A ) ; :: thesis: ( for q12, q21 being Function
for O12 being Function of (Outbds CPNT1), the carrier of CPNT2
for O21 being Function of (Outbds CPNT2), the carrier of CPNT1 holds
( not O = [O12,O21] or not dom q12 = Outbds CPNT1 or not dom q21 = Outbds CPNT2 or ex t01 being transition of CPNT1 st
( t01 is outbound & q12 . t01 is not Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) or ex t02 being transition of CPNT2 st
( t02 is outbound & q21 . t02 is not Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) or not q = [q12,q21] or not the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 or not the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 or not the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 or not the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 or not the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 or not the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) or CA = CB )
then consider q12A, q21A being Function, O12A being Function of (Outbds CPNT1), the carrier of CPNT2, O21A being Function of (Outbds CPNT2), the carrier of CPNT1 such that
A75: O = [O12A,O21A] and
dom q12A = Outbds CPNT1 and
dom q21A = Outbds CPNT2 and
for t01 being transition of CPNT1 st t01 is outbound holds
q12A . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12A,t01)))) and
for t02 being transition of CPNT2 st t02 is outbound holds
q21A . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21A,t02)))) and
A76: q = [q12A,q21A] and
A77: the carrier of CA = the carrier of CPNT1 \/ the carrier of CPNT2 and
A78: the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 and
A79: the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 and
A80: the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A and
A81: the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 and
A82: the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12A) +* q21A ;
assume ex q12B, q21B being Function ex O12B being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21B being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12B,O21B] & dom q12B = Outbds CPNT1 & dom q21B = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12B . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12B,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21B . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21B,t02)))) ) & q = [q12B,q21B] & the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B & the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12B) +* q21B ) ; :: thesis: CA = CB
then consider q12B, q21B being Function, O12B being Function of (Outbds CPNT1), the carrier of CPNT2, O21B being Function of (Outbds CPNT2), the carrier of CPNT1 such that
A83: O = [O12B,O21B] and
dom q12B = Outbds CPNT1 and
dom q21B = Outbds CPNT2 and
for t01 being transition of CPNT1 st t01 is outbound holds
q12B . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12B,t01)))) and
for t02 being transition of CPNT2 st t02 is outbound holds
q21B . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21B,t02)))) and
A84: q = [q12B,q21B] and
A85: the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 and
A86: the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 and
A87: the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 and
A88: the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B and
A89: the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 and
A90: the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12B) +* q21B ;
A91: q21A = q21B by A76, A84, XTUPLE_0:1;
A92: O12A = O12B by A75, A83, XTUPLE_0:1;
q12A = q12B by A76, A84, XTUPLE_0:1;
hence CA = CB by A75, A77, A78, A79, A80, A81, A82, A83, A85, A86, A87, A88, A89, A90, A91, A92, XTUPLE_0:1; :: thesis: verum