begin
:: deftheorem Def1 defines cylinder0 PETRI_2:def 1 :
definition
let A be non
empty set ;
let B be
set ;
mode thin_cylinder of
A,
B -> non
empty Subset of
(Funcs B,A) means :
Def2:
ex
Bo being
Subset of
B ex
yo being
Function of
Bo,
A st
(
Bo is
finite &
it = cylinder0 A,
B,
Bo,
yo );
existence
ex b1 being non empty Subset of (Funcs B,A) ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & b1 = cylinder0 A,B,Bo,yo )
end;
:: deftheorem Def2 defines thin_cylinder PETRI_2:def 2 :
theorem Th1:
theorem
:: deftheorem defines thin_cylinders PETRI_2:def 3 :
Lm1:
for A being non empty set
for B, C being set st B c= C holds
thin_cylinders A,B c= bool (PFuncs C,A)
Lm2:
for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
Lm3:
for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
Lm4:
for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
theorem Th3:
theorem Th4:
for
A1,
A2 being non
empty set for
B1,
B2 being
set st
A1 c= A2 &
B1 c= B2 holds
ex
F being
Function of
(thin_cylinders A1,B1),
(thin_cylinders A2,B2) st
for
x being
set st
x in thin_cylinders A1,
B1 holds
ex
Bo being
Subset of
B1 ex
yo1 being
Function of
Bo,
A1 ex
yo2 being
Function of
Bo,
A2 st
(
Bo is
finite &
yo1 = yo2 &
x = cylinder0 A1,
B1,
Bo,
yo1 &
F . x = cylinder0 A2,
B2,
Bo,
yo2 )
theorem Th5:
for
A1,
A2 being non
empty set for
B1,
B2 being
set ex
G being
Function of
(thin_cylinders A2,B2),
(thin_cylinders A1,B1) st
for
x being
set st
x in thin_cylinders A2,
B2 holds
ex
Bo2 being
Subset of
B2 ex
Bo1 being
Subset of
B1 ex
yo1 being
Function of
Bo1,
A1 ex
yo2 being
Function of
Bo2,
A2 st
(
Bo1 is
finite &
Bo2 is
finite &
Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) &
yo1 = yo2 | Bo1 &
x = cylinder0 A2,
B2,
Bo2,
yo2 &
G . x = cylinder0 A1,
B1,
Bo1,
yo1 )
definition
let A1,
A2 be non
trivial set ;
let B1,
B2 be
set ;
assume that A1:
A1 c= A2
and A2:
B1 c= B2
;
func Extcylinders A1,
B1,
A2,
B2 -> Function of
(thin_cylinders A1,B1),
(thin_cylinders A2,B2) means
for
x being
set st
x in thin_cylinders A1,
B1 holds
ex
Bo being
Subset of
B1 ex
yo1 being
Function of
Bo,
A1 ex
yo2 being
Function of
Bo,
A2 st
(
Bo is
finite &
yo1 = yo2 &
x = cylinder0 A1,
B1,
Bo,
yo1 &
it . x = cylinder0 A2,
B2,
Bo,
yo2 );
existence
ex b1 being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) st
for x being set st x in thin_cylinders A1,B1 holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 A1,B1,Bo,yo1 & b1 . x = cylinder0 A2,B2,Bo,yo2 )
by A1, A2, Th4;
uniqueness
for b1, b2 being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) st ( for x being set st x in thin_cylinders A1,B1 holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 A1,B1,Bo,yo1 & b1 . x = cylinder0 A2,B2,Bo,yo2 ) ) & ( for x being set st x in thin_cylinders A1,B1 holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 A1,B1,Bo,yo1 & b2 . x = cylinder0 A2,B2,Bo,yo2 ) ) holds
b1 = b2
end;
:: deftheorem defines Extcylinders PETRI_2:def 4 :
for
A1,
A2 being non
trivial set for
B1,
B2 being
set st
A1 c= A2 &
B1 c= B2 holds
for
b5 being
Function of
(thin_cylinders A1,B1),
(thin_cylinders A2,B2) holds
(
b5 = Extcylinders A1,
B1,
A2,
B2 iff for
x being
set st
x in thin_cylinders A1,
B1 holds
ex
Bo being
Subset of
B1 ex
yo1 being
Function of
Bo,
A1 ex
yo2 being
Function of
Bo,
A2 st
(
Bo is
finite &
yo1 = yo2 &
x = cylinder0 A1,
B1,
Bo,
yo1 &
b5 . x = cylinder0 A2,
B2,
Bo,
yo2 ) );
definition
let A1 be non
empty set ;
let A2 be non
trivial set ;
let B1,
B2 be
set ;
func Ristcylinders A1,
B1,
A2,
B2 -> Function of
(thin_cylinders A2,B2),
(thin_cylinders A1,B1) means
for
x being
set st
x in thin_cylinders A2,
B2 holds
ex
Bo2 being
Subset of
B2 ex
Bo1 being
Subset of
B1 ex
yo1 being
Function of
Bo1,
A1 ex
yo2 being
Function of
Bo2,
A2 st
(
Bo1 is
finite &
Bo2 is
finite &
Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) &
yo1 = yo2 | Bo1 &
x = cylinder0 A2,
B2,
Bo2,
yo2 &
it . x = cylinder0 A1,
B1,
Bo1,
yo1 );
existence
ex b1 being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) st
for x being set st x in thin_cylinders A2,B2 holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 A2,B2,Bo2,yo2 & b1 . x = cylinder0 A1,B1,Bo1,yo1 )
by Th5;
uniqueness
for b1, b2 being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) st ( for x being set st x in thin_cylinders A2,B2 holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 A2,B2,Bo2,yo2 & b1 . x = cylinder0 A1,B1,Bo1,yo1 ) ) & ( for x being set st x in thin_cylinders A2,B2 holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 A2,B2,Bo2,yo2 & b2 . x = cylinder0 A1,B1,Bo1,yo1 ) ) holds
b1 = b2
end;
:: deftheorem defines Ristcylinders PETRI_2:def 5 :
for
A1 being non
empty set for
A2 being non
trivial set for
B1,
B2 being
set for
b5 being
Function of
(thin_cylinders A2,B2),
(thin_cylinders A1,B1) holds
(
b5 = Ristcylinders A1,
B1,
A2,
B2 iff for
x being
set st
x in thin_cylinders A2,
B2 holds
ex
Bo2 being
Subset of
B2 ex
Bo1 being
Subset of
B1 ex
yo1 being
Function of
Bo1,
A1 ex
yo2 being
Function of
Bo2,
A2 st
(
Bo1 is
finite &
Bo2 is
finite &
Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) &
yo1 = yo2 | Bo1 &
x = cylinder0 A2,
B2,
Bo2,
yo2 &
b5 . x = cylinder0 A1,
B1,
Bo1,
yo1 ) );
definition
let A be non
trivial set ;
let B be
set ;
let D be
thin_cylinder of
A,
B;
func loc D -> finite Subset of
B means
ex
Bo being
Subset of
B ex
yo being
Function of
Bo,
A st
(
Bo is
finite &
D = { y where y is Function of B,A : y | Bo = yo } &
it = Bo );
existence
ex b1 being finite Subset of B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b1 = Bo )
uniqueness
for b1, b2 being finite Subset of B st ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b1 = Bo ) & ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b2 = Bo ) holds
b1 = b2
by Lm4;
end;
:: deftheorem defines loc PETRI_2:def 6 :
begin
definition
let A1,
A2 be non
trivial set ;
let B1,
B2 be
set ;
let C1,
C2 be non
trivial set ;
let D1,
D2 be
set ;
let F be
Function of
(thin_cylinders A1,B1),
(thin_cylinders C1,D1);
func CylinderFunc A1,
B1,
A2,
B2,
C1,
D1,
C2,
D2,
F -> Function of
(thin_cylinders A2,B2),
(thin_cylinders C2,D2) equals
((Extcylinders C1,D1,C2,D2) * F) * (Ristcylinders A1,B1,A2,B2);
correctness
coherence
((Extcylinders C1,D1,C2,D2) * F) * (Ristcylinders A1,B1,A2,B2) is Function of (thin_cylinders A2,B2),(thin_cylinders C2,D2);
;
end;
:: deftheorem defines CylinderFunc PETRI_2:def 7 :
for
A1,
A2 being non
trivial set for
B1,
B2 being
set for
C1,
C2 being non
trivial set for
D1,
D2 being
set for
F being
Function of
(thin_cylinders A1,B1),
(thin_cylinders C1,D1) holds
CylinderFunc A1,
B1,
A2,
B2,
C1,
D1,
C2,
D2,
F = ((Extcylinders C1,D1,C2,D2) * F) * (Ristcylinders A1,B1,A2,B2);
:: deftheorem Def8 defines outbound PETRI_2:def 8 :
:: deftheorem defines Outbds PETRI_2:def 9 :
:: deftheorem Def10 defines Colored-PT-net-like PETRI_2:def 10 :
theorem
theorem Th7:
Lm5:
for f1, f2, f3, f4, g being Function st (dom f1) /\ (dom f2) = {} & (dom f1) /\ (dom f3) = {} & (dom f1) /\ (dom f4) = {} & (dom f2) /\ (dom f3) = {} & (dom f2) /\ (dom f4) = {} & (dom f3) /\ (dom f4) = {} & g = ((f1 +* f2) +* f3) +* f4 holds
( ( for x being set st x in dom f1 holds
g . x = f1 . x ) & ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )
Lm6:
for A, B, C, D, X1, X2, X3, X4 being set st A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D holds
( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
begin
:: deftheorem Def11 defines misses PETRI_2:def 11 :
begin
:: deftheorem Def12 defines connecting-mapping PETRI_2:def 12 :
begin
definition
let CPNT1,
CPNT2 be
Colored-PT-net;
let O be
connecting-mapping of
CPNT1,
CPNT2;
mode connecting-firing-rule of
CPNT1,
CPNT2,
O -> set means :
Def13:
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)) ) &
it = [q12,q21] );
correctness
existence
ex b1 being set 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)) ) & b1 = [q12,q21] );
end;
:: deftheorem Def13 defines connecting-firing-rule PETRI_2:def 13 :
for
CPNT1,
CPNT2 being
Colored-PT-net for
O being
connecting-mapping of
CPNT1,
CPNT2 for
b4 being
set holds
(
b4 is
connecting-firing-rule of
CPNT1,
CPNT2,
O iff 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)) ) &
b4 = [q12,q21] ) );
begin
definition
let CPNT1,
CPNT2 be
Colored-PT-net;
let O be
connecting-mapping of
CPNT1,
CPNT2;
let q be
connecting-firing-rule of
CPNT1,
CPNT2,
O;
assume A1:
CPNT1 misses CPNT2
;
func synthesis CPNT1,
CPNT2,
O,
q -> strict Colored-PT-net means
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
it = the
Places of
CPNT1 \/ the
Places of
CPNT2 & the
Transitions of
it = the
Transitions of
CPNT1 \/ the
Transitions of
CPNT2 & the
S-T_Arcs of
it = the
S-T_Arcs of
CPNT1 \/ the
S-T_Arcs of
CPNT2 & the
T-S_Arcs of
it = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the
ColoredSet of
it = the
ColoredSet of
CPNT1 \/ the
ColoredSet of
CPNT2 & the
firing-rule of
it = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 );
existence
ex b1 being strict Colored-PT-net 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 b1 = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of b1 = the Transitions of CPNT1 \/ the Transitions 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 )
uniqueness
for b1, b2 being strict Colored-PT-net st 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 b1 = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of b1 = the Transitions of CPNT1 \/ the Transitions 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 ) & 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 b2 = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of b2 = the Transitions of CPNT1 \/ the Transitions of CPNT2 & the S-T_Arcs of b2 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b2 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b2 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b2 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) holds
b1 = b2
end;
:: deftheorem defines synthesis PETRI_2:def 14 :
for
CPNT1,
CPNT2 being
Colored-PT-net for
O being
connecting-mapping of
CPNT1,
CPNT2 for
q being
connecting-firing-rule of
CPNT1,
CPNT2,
O st
CPNT1 misses CPNT2 holds
for
b5 being
strict Colored-PT-net holds
(
b5 = synthesis CPNT1,
CPNT2,
O,
q iff 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
b5 = the
Places of
CPNT1 \/ the
Places of
CPNT2 & the
Transitions of
b5 = the
Transitions of
CPNT1 \/ the
Transitions of
CPNT2 & the
S-T_Arcs of
b5 = the
S-T_Arcs of
CPNT1 \/ the
S-T_Arcs of
CPNT2 & the
T-S_Arcs of
b5 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the
ColoredSet of
b5 = the
ColoredSet of
CPNT1 \/ the
ColoredSet of
CPNT2 & the
firing-rule of
b5 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) );