:: Cell Petri Net Concepts
:: by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,
::
:: Received October 14, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let A be non empty set ;
let B, Bo be set ;
let yo be Function of Bo,A;
assume A1: Bo c= B ;
func cylinder0 (A,B,Bo,yo) -> non empty Subset of (Funcs (B,A)) equals :Def1: :: PETRI_2:def 1
{ y where y is Function of B,A : y | Bo = yo } ;
correctness
coherence
{ y where y is Function of B,A : y | Bo = yo } is non empty Subset of (Funcs (B,A))
;
proof end;
end;

:: deftheorem Def1 defines cylinder0 PETRI_2:def 1 :
for A being non empty set
for B, Bo being set
for yo being Function of Bo,A st Bo c= B holds
cylinder0 (A,B,Bo,yo) = { y where y is Function of B,A : y | Bo = yo } ;

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: :: PETRI_2:def 2
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) )
proof end;
end;

:: deftheorem Def2 defines thin_cylinder PETRI_2:def 2 :
for A being non empty set
for B being set
for b3 being non empty Subset of (Funcs (B,A)) holds
( b3 is thin_cylinder of A,B iff ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & b3 = cylinder0 (A,B,Bo,yo) ) );

theorem Th1: :: PETRI_2:1
for A being non empty set
for B being set
for D being thin_cylinder of A,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 } )
proof end;

theorem :: PETRI_2:2
for A1, A2 being non empty set
for B being set
for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
proof end;

definition
let A be non empty set ;
let B be set ;
func thin_cylinders (A,B) -> non empty Subset-Family of (Funcs (B,A)) equals :: PETRI_2:def 3
{ D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;
correctness
coherence
{ D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } is non empty Subset-Family of (Funcs (B,A))
;
proof end;
end;

:: deftheorem defines thin_cylinders PETRI_2:def 3 :
for A being non empty set
for B being set holds thin_cylinders (A,B) = { D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;

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))

proof end;

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 )

proof end;

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 )

proof end;

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 }

proof end;

theorem Th3: :: PETRI_2:3
for A being non trivial set
for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
proof end;

theorem Th4: :: PETRI_2:4
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) )
proof end;

theorem Th5: :: PETRI_2:5
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) )
proof end;

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 :: PETRI_2:def 4
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
proof end;
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 :: PETRI_2:def 5
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
proof end;
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 :: PETRI_2:def 6
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 )
proof end;
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 :
for A being non trivial set
for B being set
for D being thin_cylinder of A,B
for b4 being finite Subset of B holds
( b4 = loc D iff 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 } & b4 = Bo ) );

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 :: PETRI_2:def 7
((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));

definition
attr c1 is strict ;
struct Colored_PT_net_Str -> PT_net_Str ;
aggr Colored_PT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs, ColoredSet, firing-rule #) -> Colored_PT_net_Str ;
sel ColoredSet c1 -> non empty finite set ;
sel firing-rule c1 -> Function;
end;

definition
func TrivialColoredPetriNet -> Colored_PT_net_Str equals :: PETRI_2:def 8
Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);
coherence
Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #) is Colored_PT_net_Str
;
end;

:: deftheorem defines TrivialColoredPetriNet PETRI_2:def 8 :
TrivialColoredPetriNet = Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

registration
cluster TrivialColoredPetriNet -> non empty non void with_S-T_arc with_T-S_arc ;
coherence
( TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
proof end;
end;

registration
cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str ;
existence
ex b1 being Colored_PT_net_Str st
( not b1 is empty & not b1 is void & b1 is with_S-T_arc & b1 is with_T-S_arc )
proof end;
end;

definition
mode Colored_Petri_net is non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str ;
end;

definition
let CPNT be Colored_Petri_net;
let t0 be transition of CPNT;
attr t0 is outbound means :Def9: :: PETRI_2:def 9
{t0} *' = {} ;
end;

:: deftheorem Def9 defines outbound PETRI_2:def 9 :
for CPNT being Colored_Petri_net
for t0 being transition of CPNT holds
( t0 is outbound iff {t0} *' = {} );

definition
let CPNT1 be Colored_Petri_net;
func Outbds CPNT1 -> Subset of the carrier' of CPNT1 equals :: PETRI_2:def 10
{ x where x is transition of CPNT1 : x is outbound } ;
coherence
{ x where x is transition of CPNT1 : x is outbound } is Subset of the carrier' of CPNT1
proof end;
end;

:: deftheorem defines Outbds PETRI_2:def 10 :
for CPNT1 being Colored_Petri_net holds Outbds CPNT1 = { x where x is transition of CPNT1 : x is outbound } ;

definition
let CPNT be Colored_Petri_net;
attr CPNT is Colored-PT-net-like means :Def11: :: PETRI_2:def 11
( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) );
end;

:: deftheorem Def11 defines Colored-PT-net-like PETRI_2:def 11 :
for CPNT being Colored_Petri_net holds
( CPNT is Colored-PT-net-like iff ( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) ) );

theorem :: PETRI_2:6
for CPNT being Colored_Petri_net
for t being transition of CPNT st CPNT is Colored-PT-net-like & t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by Def11;

theorem Th7: :: PETRI_2:7
for CPNT1, CPNT2 being Colored_Petri_net
for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
proof end;

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 ) )

proof end;

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 = {} )

proof end;

registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc strict Colored-PT-net-like for Colored_PT_net_Str ;
existence
ex b1 being Colored_Petri_net st
( b1 is strict & b1 is Colored-PT-net-like )
proof end;
end;

definition
mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;
end;

begin

definition
let CPNT1, CPNT2 be Colored_Petri_net;
pred CPNT1 misses CPNT2 means :Def12: :: PETRI_2:def 12
( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} );
symmetry
for CPNT1, CPNT2 being Colored_Petri_net st the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} holds
( the carrier of CPNT2 /\ the carrier of CPNT1 = {} & the carrier' of CPNT2 /\ the carrier' of CPNT1 = {} )
;
end;

:: deftheorem Def12 defines misses PETRI_2:def 12 :
for CPNT1, CPNT2 being Colored_Petri_net holds
( CPNT1 misses CPNT2 iff ( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} ) );

begin

definition
let CPNT1, CPNT2 be Colored_Petri_net;
mode connecting-mapping of CPNT1,CPNT2 -> set means :Def13: :: PETRI_2:def 13
ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st it = [O12,O21];
correctness
existence
ex b1 being set ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st b1 = [O12,O21]
;
proof end;
end;

:: deftheorem Def13 defines connecting-mapping PETRI_2:def 13 :
for CPNT1, CPNT2 being Colored_Petri_net
for b3 being set holds
( b3 is connecting-mapping of CPNT1,CPNT2 iff ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st b3 = [O12,O21] );

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 :Def14: :: PETRI_2:def 14
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)))) ) & it = [q12,q21] );
correctness
existence
ex b1 being set 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)))) ) & b1 = [q12,q21] )
;
proof end;
end;

:: deftheorem Def14 defines connecting-firing-rule PETRI_2:def 14 :
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 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)))) ) & 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 :: PETRI_2:def 15
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 it = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of it = the carrier' of CPNT1 \/ the carrier' 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 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 )
proof end;
uniqueness
for b1, b2 being strict Colored-PT-net st 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 ) & 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 b2 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b2 = the carrier' of CPNT1 \/ the carrier' 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
proof end;
end;

:: deftheorem defines synthesis PETRI_2:def 15 :
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 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 b5 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b5 = the carrier' of CPNT1 \/ the carrier' 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 ) );