:: by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,

::

:: Received October 14, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

definition

let A be non empty set ;

let B, Bo be set ;

let yo be Function of Bo,A;

assume A1: Bo c= B ;

coherence

{ y where y is Function of B,A : y | Bo = yo } is non empty Subset of (Funcs (B,A));

end;
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 { y where y is Function of B,A : y | Bo = yo } ;

coherence

{ y where y is Function of B,A : y | Bo = yo } is non empty Subset of (Funcs (B,A));

proof 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 } ;

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 ;

ex b_{1} 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 & b_{1} = cylinder0 (A,B,Bo,yo) )

end;
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 Bo being Subset of B ex yo being Function of Bo,A st

( Bo is finite & it = cylinder0 (A,B,Bo,yo) );

ex b

( Bo is finite & b

proof end;

:: deftheorem Def2 defines thin_cylinder PETRI_2:def 2 :

for A being non empty set

for B being set

for b_{3} being non empty Subset of (Funcs (B,A)) holds

( b_{3} is thin_cylinder of A,B iff ex Bo being Subset of B ex yo being Function of Bo,A st

( Bo is finite & b_{3} = cylinder0 (A,B,Bo,yo) ) );

for A being non empty set

for B being set

for b

( b

( Bo is finite & b

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

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

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 ;

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

end;
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 { D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;

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;

:: 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 } ;

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 )

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

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

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 ;

ex b_{1} 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) & b_{1} . x = cylinder0 (A2,B2,Bo,yo2) )
by A1, A2, Th4;

uniqueness

for b_{1}, b_{2} 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) & b_{1} . 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) & b_{2} . x = cylinder0 (A2,B2,Bo,yo2) ) ) holds

b_{1} = b_{2}

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

ex b

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

uniqueness

for b

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

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

b

proof 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 b_{5} being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) holds

( b_{5} = 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) & b_{5} . x = cylinder0 (A2,B2,Bo,yo2) ) );

for A1, A2 being non trivial set

for B1, B2 being set st A1 c= A2 & B1 c= B2 holds

for b

( b

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

definition

let A1 be non empty set ;

let A2 be non trivial set ;

let B1, B2 be set ;

ex b_{1} 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) & b_{1} . x = cylinder0 (A1,B1,Bo1,yo1) )
by Th5;

uniqueness

for b_{1}, b_{2} 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) & b_{1} . 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) & b_{2} . x = cylinder0 (A1,B1,Bo1,yo1) ) ) holds

b_{1} = b_{2}

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

ex b

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

uniqueness

for b

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

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

b

proof 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 b_{5} being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) holds

( b_{5} = 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) & b_{5} . x = cylinder0 (A1,B1,Bo1,yo1) ) );

for A1 being non empty set

for A2 being non trivial set

for B1, B2 being set

for b

( b

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

definition

let A be non trivial set ;

let B be set ;

let D be thin_cylinder of A,B;

ex b_{1} 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 } & b_{1} = Bo )

for b_{1}, b_{2} 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 } & b_{1} = 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 } & b_{2} = Bo ) holds

b_{1} = b_{2}
by Lm4;

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

ex b

( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b

proof end;

uniqueness for b

( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b

( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b

b

:: 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 b_{4} being finite Subset of B holds

( b_{4} = 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 } & b_{4} = Bo ) );

for A being non trivial set

for B being set

for D being thin_cylinder of A,B

for b

( b

( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b

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

coherence

((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2)) is Function of (thin_cylinders (A2,B2)),(thin_cylinders (C2,D2));

;

end;
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 ((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2));

coherence

((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2)) is Function of (thin_cylinders (A2,B2)),(thin_cylinders (C2,D2));

;

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

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 c_{1} 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 c_{1} -> non empty finite set ;

sel firing-rule c_{1} -> Function;

end;
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 c

sel firing-rule c

definition

Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #) is Colored_PT_net_Str ;

end;

func TrivialColoredPetriNet -> Colored_PT_net_Str equals :: PETRI_2:def 8

Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

coherence Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #) is Colored_PT_net_Str ;

:: deftheorem defines TrivialColoredPetriNet PETRI_2:def 8 :

TrivialColoredPetriNet = Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

TrivialColoredPetriNet = Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

registration

coherence

( TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void ) ;

end;
( TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void ) ;

registration

existence

ex b_{1} being Colored_PT_net_Str st

( not b_{1} is empty & not b_{1} is void & b_{1} is with_S-T_arc & b_{1} is with_T-S_arc )

end;
ex b

( not b

proof end;

definition
end;

:: deftheorem defines outbound PETRI_2:def 9 :

for CPNT being Colored_Petri_net

for t0 being transition of CPNT holds

( t0 is outbound iff {t0} *' = {} );

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;

{ x where x is transition of CPNT1 : x is outbound } is Subset of the carrier' of CPNT1

end;
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 } ;

{ x where x is transition of CPNT1 : x is outbound } is Subset of the carrier' of CPNT1

proof 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 } ;

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;

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

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

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

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

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

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} *' )

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

ex b_{1} being Colored_Petri_net st

( b_{1} is strict & b_{1} is Colored-PT-net-like )
end;

cluster non empty non void V52() with_S-T_arc with_T-S_arc strict Colored-PT-net-like for Colored_PT_net_Str ;

existence ex b

( b

proof end;

definition

let CPNT1, CPNT2 be Colored_Petri_net;

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;
pred CPNT1 misses CPNT2 means :: PETRI_2:def 12

( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} );

symmetry ( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} );

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

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

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

definition

let CPNT1, CPNT2 be Colored_Petri_net;

existence

ex b_{1} 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 b_{1} = [O12,O21];

end;
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 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];

existence

ex b

proof end;

:: deftheorem Def13 defines connecting-mapping PETRI_2:def 13 :

for CPNT1, CPNT2 being Colored_Petri_net

for b_{3} being set holds

( b_{3} 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 b_{3} = [O12,O21] );

for CPNT1, CPNT2 being Colored_Petri_net

for b

( b

definition

let CPNT1, CPNT2 be Colored-PT-net;

let O be connecting-mapping of CPNT1,CPNT2;

existence

ex b_{1} 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)))) ) & b_{1} = [q12,q21] );

end;
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 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] );

existence

ex b

( 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)))) ) & b

proof 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 b_{4} being set holds

( b_{4} 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)))) ) & b_{4} = [q12,q21] ) );

for CPNT1, CPNT2 being Colored-PT-net

for O being connecting-mapping of CPNT1,CPNT2

for b

( b

( 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)))) ) & b

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 ;

ex b_{1} 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 b_{1} = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b_{1} = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b_{1} = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b_{1} = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b_{1} = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b_{1} = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 )

for b_{1}, b_{2} 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 b_{1} = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b_{1} = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b_{1} = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b_{1} = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b_{1} = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b_{1} = (( 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 b_{2} = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b_{2} = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b_{2} = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b_{2} = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b_{2} = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b_{2} = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) holds

b_{1} = b_{2}

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

ex b

( 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 b

proof end;

uniqueness for b

( 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 b

( 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 b

b

proof 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 b_{5} being strict Colored-PT-net holds

( b_{5} = 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 b_{5} = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b_{5} = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b_{5} = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b_{5} = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b_{5} = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b_{5} = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) );

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 b

( b

( 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 b