let CA, CB be strict Colored-PT-net; :: thesis: ( ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1),the Places of CPNT2 ex O21 being Function of (Outbds CPNT2),the Places 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 Places of CA = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CA = the Transitions of CPNT1 \/ the Transitions 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 Places of CPNT2 ex O21 being Function of (Outbds CPNT2),the Places 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 Places of CB = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CB = the Transitions of CPNT1 \/ the Transitions 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 AS1: ex q12A, q21A being Function ex O12A being Function of (Outbds CPNT1),the Places of CPNT2 ex O21A being Function of (Outbds CPNT2),the Places 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 Places of CA = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CA = the Transitions of CPNT1 \/ the Transitions 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 Places of CPNT2
for O21 being Function of (Outbds CPNT2),the Places 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 Places of CB = the Places of CPNT1 \/ the Places of CPNT2 or not the Transitions of CB = the Transitions of CPNT1 \/ the Transitions 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 )
assume BS1: ex q12B, q21B being Function ex O12B being Function of (Outbds CPNT1),the Places of CPNT2 ex O21B being Function of (Outbds CPNT2),the Places 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 Places of CB = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CB = the Transitions of CPNT1 \/ the Transitions 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
consider q12A, q21A being Function, O12A being Function of (Outbds CPNT1),the Places of CPNT2, O21A being Function of (Outbds CPNT2),the Places of CPNT1 such that
P1: ( 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 Places of CA = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CA = the Transitions of CPNT1 \/ the Transitions 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 ) by AS1;
consider q12B, q21B being Function, O12B being Function of (Outbds CPNT1),the Places of CPNT2, O21B being Function of (Outbds CPNT2),the Places of CPNT1 such that
P2: ( 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 Places of CB = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of CB = the Transitions of CPNT1 \/ the Transitions 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 ) by BS1;
P3: ( q12A = q12B & q21A = q21B ) by P1, P2, ZFMISC_1:33;
( O12A = O12B & O21A = O21B ) by P1, P2, ZFMISC_1:33;
hence CA = CB by P1, P2, P3; :: thesis: verum