:: Cell Petri Net Concepts
:: by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,
:: and Yatsuka Nakamura
::
:: Received October 14, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PETRI, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_2, RELAT_1,
FUNCOP_1, FUNCT_4, FINSET_1, SETFAM_1, ZFMISC_1, PARTFUN1, ARYTM_3,
CARD_1, PETRI_2, STRUCT_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, SETFAM_1, RELAT_1,
RELSET_1, DOMAIN_1, PETRI, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, RELSET_2,
FINSET_1, FUNCOP_1, ORDINAL1, CARD_1, PARTIT_2, STRUCT_0;
constructors RELSET_1, DOMAIN_1, PETRI, RELSET_2, FUNCT_4, PARTIT_2, FUNCOP_1;
registrations SUBSET_1, RELAT_1, PARTFUN1, RELSET_1, XBOOLE_0, FUNCT_2,
FINSET_1, STRUCT_0, FUNCT_1, PETRI, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities PETRI;
expansions TARSKI, PETRI;
theorems RELSET_1, PARTFUN1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, PETRI,
FUNCT_1, FUNCT_2, XBOOLE_1, FUNCT_4, FUNCOP_1, RELSET_2, XTUPLE_0;
schemes FUNCT_2;
begin :: Preliminaries: thin cylinder, locus
definition
let A be non empty set, B be set;
let Bo be set, 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:
{ y where y is Function of B,A : y|Bo = yo };
correctness
proof
set D = { y where y is Function of B,A : y|Bo = yo };
A2: now
per cases;
suppose
A3: Bo = {};
set f = the Function of B,A;
f|{} = {} .= yo by A3;
then f in D by A3;
hence D is non empty;
end;
suppose
Bo <> {};
then consider b0 be object such that
A4: b0 in Bo by XBOOLE_0:def 1;
yo.b0 in A by A4,FUNCT_2:5;
then
A5: {yo.b0} c= A by ZFMISC_1:31;
set f = (B --> yo.b0) +* yo;
A6: rng f c= rng(B --> yo.b0) \/ rng yo by FUNCT_4:17;
A7: rng yo c= A by RELAT_1:def 19;
A8: dom yo = Bo by FUNCT_2:def 1;
then
A9: dom f = dom(B --> yo.b0) \/ Bo by FUNCT_4:def 1
.= B \/ Bo by FUNCOP_1:13
.= B by A1,XBOOLE_1:12;
rng(B --> yo.b0) c= {yo.b0} by FUNCOP_1:13;
then rng(B --> yo.b0) c= A by A5;
then rng(B --> yo.b0) \/ rng yo c= A by A7,XBOOLE_1:8;
then reconsider f as Function of B,A by A6,A9,FUNCT_2:2,XBOOLE_1:1;
f|Bo = yo by A8,FUNCT_4:23;
then f in D;
hence D is non empty;
end;
end;
now
let z be object;
assume z in D;
then ex y be Function of B,A st z=y & y|Bo = yo;
hence z in Funcs(B,A) by FUNCT_2:8;
end;
hence thesis by A2,TARSKI:def 3;
end;
end;
definition
let A be non empty set, B be set;
mode thin_cylinder of A,B -> non empty Subset of Funcs(B,A) means
:Def2:
ex
Bo being Subset of B,yo being Function of Bo,A st Bo is finite & it = cylinder0
(A,B,Bo,yo);
existence
proof
set Bo={};
set yo = the Function of Bo,A;
take cylinder0(A,B,Bo,yo);
Bo is Subset of B by XBOOLE_1:2;
hence thesis;
end;
end;
theorem Th1:
for A be non empty set, B be set, D be thin_cylinder of A,B holds
ex Bo being Subset of B,yo being Function of Bo,A st Bo is finite & D = { y
where y is Function of B,A : y|Bo = yo }
proof
let A be non empty set, B be set, D be thin_cylinder of A,B;
consider Bo being Subset of B,yo being Function of Bo,A such that
A1: Bo is finite and
A2: D = cylinder0(A,B,Bo,yo) by Def2;
D = { y where y is Function of B,A : y|Bo = yo } by A2,Def1;
hence thesis by A1;
end;
theorem
for A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1,B st
A1 c= A2 ex D2 be thin_cylinder of A2,B st D1 c= D2
proof
let A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1,B;
consider Bo being Subset of B,yo1 being Function of Bo,A1 such that
A1: Bo is finite and
A2: D1 = { y where y is Function of B,A1: y|Bo = yo1 } by Th1;
assume
A3: A1 c= A2;
then reconsider yo2=yo1 as Function of Bo,A2 by FUNCT_2:7;
set D2= { y where y is Function of B,A2: y|Bo = yo2 };
A4: now
let x be object;
assume x in D1;
then consider y1 be Function of B,A1 such that
A5: x=y1 and
A6: y1|Bo = yo1 by A2;
reconsider y2=y1 as Function of B,A2 by A3,FUNCT_2:7;
y2|Bo = yo1 by A6;
hence x in D2 by A5;
end;
D2= cylinder0(A2,B,Bo,yo2) by Def1;
then reconsider D2 as thin_cylinder of A2,B by A1,Def2;
take D2;
thus thesis by A4;
end;
definition
let A be non empty set, B be set;
func thin_cylinders(A,B) -> non empty Subset-Family of Funcs(B,A) equals
{D
where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
correctness
proof
set F = the thin_cylinder of A,B;
A1: now
let z be object;
assume
z in {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
then ex D be Subset of Funcs(B,A) st z=D & D is thin_cylinder of A,B;
hence z in bool Funcs(B,A);
end;
F in {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
hence thesis by A1,TARSKI:def 3;
end;
end;
Lm1: for A be non empty set, B,C be set st B c= C holds thin_cylinders(A,B) c=
bool PFuncs(C,A)
proof
let A be non empty set, B,C be set;
assume B c= C;
then
A1: PFuncs(B,A) c= PFuncs(C,A) by PARTFUN1:50;
Funcs(B,A) c= PFuncs(B,A) by FUNCT_2:72;
then Funcs(B,A) c= PFuncs(C,A) by A1;
then
A2: bool Funcs(B,A) c= bool PFuncs(C,A) by ZFMISC_1:67;
let x be object;
assume x in thin_cylinders(A,B);
then consider D be Subset of Funcs(B,A) such that
A3: x=D and
D is thin_cylinder of A,B;
thus thesis by A3,A2;
end;
Lm2: for A be non trivial set,B be set, Bo1,Bo2 be Subset of B,yo1 be Function
of Bo1,A, yo2 be Function of Bo2,A st not Bo2 c= Bo1 holds ex f be Function of
B,A st f|Bo1 = yo1 & f|Bo2 <> yo2
proof
let A be non trivial set, B be set, Bo1,Bo2 be Subset of B,yo1 be Function
of Bo1,A, yo2 be Function of Bo2,A;
defpred C[object] means $1 in Bo1;
deffunc F(object) = yo1.$1;
assume not Bo2 c= Bo1;
then consider x0 be object such that
A1: x0 in Bo2 and
A2: not x0 in Bo1;
A3: x0 in dom yo2 by A1,FUNCT_2:def 1;
ex y0 be set st y0 in A & y0 <> yo2.x0
proof
consider x,y be object such that
A4: x in A and
A5: y in A and
A6: x <> y by ZFMISC_1:def 10;
per cases;
suppose
A7: yo2.x0 = x;
take y;
thus thesis by A5,A6,A7;
end;
suppose
A8: yo2.x0 <> x;
take x;
thus thesis by A4,A8;
end;
end;
then consider y0 be set such that
A9: y0 in A and
A10: y0 <> yo2.x0;
deffunc G(object) = y0;
A11: for x be object st x in B holds (C[ x] implies F(x) in A) & (not C[ x]
implies G(x) in A) by A9,FUNCT_2:5;
consider f be Function of B, A such that
A12: for x be object st x in B holds (C[ x] implies f.x = F(x)) & (not C[ x
] implies f.x = G(x)) from FUNCT_2:sch 5(A11);
A13: now
let z be object;
assume z in dom yo1;
then z in Bo1;
hence yo1.z = f.z by A12;
end;
f.x0 <> yo2.x0 by A1,A2,A10,A12;
then
A14: f|Bo2 <> yo2 by A3,FUNCT_1:47;
dom yo1 = Bo1 by FUNCT_2:def 1
.= B /\ Bo1 by XBOOLE_1:28
.= dom f /\ Bo1 by FUNCT_2:def 1;
then f|Bo1 = yo1 by A13,FUNCT_1:46;
hence thesis by A14;
end;
Lm3: for A be non trivial set, B be set, Bo1,Bo2 be Subset of B,yo1 be
Function of Bo1,A, yo2 be Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds ex
f be Function of B,A st f|Bo2 = yo2 & f|Bo1 <> yo1
proof
let A be non trivial set, B be set, Bo1,Bo2 be Subset of B,yo1 be Function
of Bo1,A, yo2 be Function of Bo2,A;
assume that
A1: Bo1 <> Bo2 and
A2: Bo2 c= Bo1;
Bo2 c< Bo1 by A1,A2,XBOOLE_0:def 8;
then consider x0 be object such that
A3: x0 in Bo1 and
A4: not x0 in Bo2 by XBOOLE_0:6;
A5: x0 in dom yo1 by A3,FUNCT_2:def 1;
deffunc F(object) = yo2.$1;
defpred C[object] means $1 in Bo2;
ex y0 be set st y0 in A & y0 <> yo1.x0
proof
consider x,y be object such that
A6: x in A and
A7: y in A and
A8: x <> y by ZFMISC_1:def 10;
per cases;
suppose
A9: yo1.x0 = x;
take y;
thus thesis by A7,A8,A9;
end;
suppose
A10: yo1.x0 <> x;
take x;
thus thesis by A6,A10;
end;
end;
then consider y0 be set such that
A11: y0 in A and
A12: y0 <> yo1.x0;
deffunc G(object) = y0;
A13: for x be object st x in B holds (C[ x] implies F(x) in A) & (not C[ x]
implies G(x) in A) by A11,FUNCT_2:5;
consider f be Function of B, A such that
A14: for x be object st x in B
holds (C[ x] implies f.x = F(x)) & (not C[ x
] implies f.x = G(x)) from FUNCT_2:sch 5(A13);
A15: now
let z be object;
assume z in dom yo2;
then z in Bo2;
hence yo2.z = f.z by A14;
end;
f.x0 <> yo1.x0 by A3,A4,A12,A14;
then
A16: f|Bo1 <> yo1 by A5,FUNCT_1:47;
dom yo2 = Bo2 by FUNCT_2:def 1
.= B /\ Bo2 by XBOOLE_1:28
.= dom f /\ Bo2 by FUNCT_2:def 1;
then f|Bo2 = yo2 by A15,FUNCT_1:46;
hence thesis by A16;
end;
Lm4: for A be non trivial set,B be set, Bo1,Bo2 be Subset of B,yo1 be Function
of Bo1,A, yo2 be 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
let A be non trivial set, B be set, Bo1,Bo2 be Subset of B,yo1 be Function
of Bo1,A, yo2 be Function of Bo2,A;
assume
A1: Bo1 <> Bo2;
per cases;
suppose
not Bo2 c= Bo1;
then consider f be Function of B,A such that
A2: f|Bo1 = yo1 and
A3: f|Bo2 <> yo2 by Lm2;
not f in { y where y is Function of B,A : y|Bo2 = yo2 }
proof
assume f in { y where y is Function of B,A : y|Bo2 = yo2 };
then ex y be Function of B,A st f=y & y|Bo2 = yo2;
hence contradiction by A3;
end;
hence thesis by A2;
end;
suppose
Bo2 c= Bo1;
then consider f be Function of B,A such that
A4: f|Bo2 = yo2 and
A5: f|Bo1 <> yo1 by A1,Lm3;
not f in { y where y is Function of B,A : y|Bo1 = yo1 }
proof
assume f in { y where y is Function of B,A : y|Bo1 = yo1 };
then ex y be Function of B,A st f=y & y|Bo1 = yo1;
hence contradiction by A5;
end;
hence thesis by A4;
end;
end;
theorem Th3:
for A be non trivial set, B be set, Bo1 be set, yo1 being
Function of Bo1,A, Bo2 be set, 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
let A be non trivial set, B be set, Bo1 be set,yo1 being Function of Bo1,A,
Bo2 be set,yo2 being Function of Bo2,A;
assume that
A1: Bo1 c= B and
A2: Bo2 c= B and
A3: cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2);
A4: { y where y is Function of B,A : y|Bo1 = yo1 } = cylinder0(A,B,Bo1,yo1)
by A1,Def1;
then consider y0 be object such that
A5: y0 in { y where y is Function of B,A : y|Bo1 = yo1 } by XBOOLE_0:def 1;
A6: ex y be Function of B,A st y0=y & y|Bo1 = yo1 by A5;
A7: { y where y is Function of B,A : y|Bo2 = yo2 } = cylinder0(A,B,Bo2,yo2)
by A2,Def1;
hence Bo1=Bo2 by A1,A2,A3,A4,Lm4;
ex w be Function of B,A st y0=w & w|Bo2 = yo2 by A3,A4,A7,A5;
hence thesis by A1,A2,A3,A4,A7,A6,Lm4;
end;
theorem Th4:
for A1,A2 be non empty set, B1,B2 be set st A1 c= A2 & B1 c= B2
ex F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) st for x be
set st x in thin_cylinders(A1,B1) ex Bo being Subset of B1, yo1 being Function
of Bo,A1, 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
let A1,A2 be non empty set, B1,B2 be set;
assume that
A1: A1 c= A2 and
A2: B1 c= B2;
defpred P[object,object] means
ex Bo being Subset of B1,yo1 being Function of Bo,
A1, yo2 being Function of Bo,A2 st Bo is finite & yo1=yo2 & $1=cylinder0(A1,B1,
Bo,yo1) & $2=cylinder0(A2,B2,Bo,yo2);
A3: now
let x be object;
assume x in thin_cylinders(A1,B1);
then
ex D be Subset of Funcs(B1,A1) st x=D & D is thin_cylinder of A1,B1;
then reconsider D1=x as thin_cylinder of A1,B1;
consider Bo being Subset of B1,yo1 being Function of Bo,A1 such that
A4: Bo is finite and
A5: D1=cylinder0(A1,B1,Bo,yo1) by Def2;
reconsider yo2=yo1 as Function of Bo,A2 by A1,FUNCT_2:7;
set D2= cylinder0(A2,B2,Bo,yo2);
Bo c= B2 by A2;
then
A6: D2 is thin_cylinder of A2,B2 by A4,Def2;
reconsider D2 as object;
take D2;
thus D2 in thin_cylinders(A2,B2) & P[x,D2] by A4,A5,A6;
end;
consider F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) such
that
A7: for x be object st x in thin_cylinders(A1,B1) holds P[x,F.x] from
FUNCT_2:sch 1(A3);
take F;
thus thesis by A7;
end;
theorem Th5:
for A1,A2 be non empty set, B1,B2 be set ex G be Function of
thin_cylinders(A2,B2), thin_cylinders(A1,B1) st for x be set st x in
thin_cylinders(A2,B2) ex Bo2 being Subset of B2,Bo1 being Subset of B1, yo1
being Function of Bo1,A1, 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
let A1,A2 be non empty set, B1,B2 be set;
defpred P[object,object] means
ex Bo2 being Subset of B2,Bo1 being Subset of B1,
yo1 being Function of Bo1,A1, yo2 being Function of Bo2,A2 st Bo1 is finite &
Bo2 is finite & Bo1=B1 /\ Bo2 /\ (yo2"A1) & yo1=yo2 | Bo1 & $1=cylinder0(A2,B2,
Bo2,yo2) & $2=cylinder0(A1,B1,Bo1,yo1);
A1: now
let x be object;
assume x in thin_cylinders(A2,B2);
then
ex D be Subset of Funcs(B2,A2) st x=D & D is thin_cylinder of A2,B2;
then reconsider D2=x as thin_cylinder of A2,B2;
consider Bo2 being Subset of B2,yo2 being Function of Bo2,A2 such that
A2: Bo2 is finite and
A3: D2=cylinder0(A2,B2,Bo2,yo2) by Def2;
set Bo1=B1 /\ Bo2 /\ (yo2"A1);
A4: Bo1 c= B1 /\ Bo2 by XBOOLE_1:17;
set yo1=yo2 | Bo1;
B1 /\ Bo2 c= Bo2 by XBOOLE_1:17;
then Bo1 c= Bo2 by A4;
then
A5: yo1 is Function of Bo1, A2 by FUNCT_2:32;
A6: rng yo1 = yo2.: Bo1 by RELAT_1:115;
A7: yo2.: Bo1 c= yo2.: (yo2"A1) by RELAT_1:123,XBOOLE_1:17;
yo2.: (yo2"A1) c= A1 by FUNCT_1:75;
then yo2.: Bo1 c= A1 by A7;
then reconsider yo1 as Function of Bo1,A1 by A5,A6,FUNCT_2:6;
set D1= cylinder0(A1,B1,Bo1,yo1);
B1 /\ Bo2 c= B1 by XBOOLE_1:17;
then
A8: Bo1 c= B1 by A4;
then
A9: D1 is thin_cylinder of A1,B1 by A2,Def2;
reconsider D1 as object;
take D1;
thus D1 in thin_cylinders(A1,B1) & P[x,D1] by A2,A3,A8,A9;
end;
consider G be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1) such
that
A10: for x be object st x in thin_cylinders(A2,B2) holds P[x,G.x] from
FUNCT_2:sch 1(A1);
take G;
thus thesis by A10;
end;
definition
let A1,A2 be non trivial set, 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 be set st x in thin_cylinders(A1,B1) ex Bo
being Subset of B1, yo1 being Function of Bo,A1, 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 by A1,A2,Th4;
uniqueness
proof
let F1,F2 be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2);
assume
A3: for x be set st x in thin_cylinders(A1,B1) ex Bo being Subset of
B1, yo1 being Function of Bo,A1, yo2 being Function of Bo,A2 st Bo is finite &
yo1=yo2 & x=cylinder0(A1,B1,Bo,yo1) & F1.x=cylinder0(A2,B2,Bo,yo2);
assume
A4: for x be set st x in thin_cylinders(A1,B1) ex Bo being Subset of
B1, yo1 being Function of Bo,A1, yo2 being Function of Bo,A2 st Bo is finite &
yo1=yo2 & x=cylinder0(A1,B1,Bo,yo1) & F2.x=cylinder0(A2,B2,Bo,yo2);
now
let x be object;
assume
A5: x in thin_cylinders(A1,B1);
then consider
Bo1 being Subset of B1, yo11 being Function of Bo1,A1, yo21
being Function of Bo1,A2 such that
Bo1 is finite and
A6: yo11=yo21 and
A7: x=cylinder0(A1,B1,Bo1,yo11) and
A8: F1.x=cylinder0(A2,B2,Bo1,yo21) by A3;
consider Bo2 being Subset of B1, yo12 being Function of Bo2,A1, yo22
being Function of Bo2,A2 such that
Bo2 is finite and
A9: yo12=yo22 and
A10: x=cylinder0(A1,B1,Bo2,yo12) and
A11: F2.x=cylinder0(A2,B2,Bo2,yo22) by A4,A5;
Bo1 = Bo2 by A7,A10,Th3;
hence F1.x=F2.x by A6,A7,A8,A9,A10,A11,Th3;
end;
hence F1=F2 by FUNCT_2:12;
end;
end;
definition
let A1 be non empty set, A2 be non trivial set, B1,B2 be set;
func Ristcylinders(A1,B1,A2,B2) -> Function of thin_cylinders(A2,B2),
thin_cylinders(A1,B1) means
for x be set st x in thin_cylinders(A2,B2) ex Bo2
being Subset of B2,Bo1 being Subset of B1, yo1 being Function of Bo1,A1, 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 by Th5;
uniqueness
proof
let F1,F2 be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1);
assume
A1: for x be set st x in thin_cylinders(A2,B2) ex Bo21 being Subset of
B2,Bo11 being Subset of B1, yo11 being Function of Bo11,A1, yo21 being Function
of Bo21,A2 st Bo11 is finite & Bo21 is finite & Bo11=B1 /\ Bo21 /\ (yo21"A1) &
yo11=yo21 | Bo11 & x= cylinder0(A2,B2,Bo21,yo21) & F1.x =cylinder0(A1,B1,Bo11,
yo11);
assume
A2: for x be set st x in thin_cylinders(A2,B2) ex Bo22 being Subset of
B2,Bo12 being Subset of B1, yo12 being Function of Bo12,A1, yo22 being Function
of Bo22,A2 st Bo12 is finite & Bo22 is finite & Bo12=B1 /\ Bo22 /\ (yo22"A1) &
yo12=yo22 | Bo12 & x= cylinder0(A2,B2,Bo22,yo22) & F2.x =cylinder0(A1,B1,Bo12,
yo12);
now
let x be object;
assume
A3: x in thin_cylinders(A2,B2);
then consider
Bo21 being Subset of B2,Bo11 being Subset of B1, yo11 being
Function of Bo11,A1, yo21 being Function of Bo21,A2 such that
Bo11 is finite and
Bo21 is finite and
A4: Bo11=B1 /\ Bo21 /\ (yo21"A1) and
A5: yo11=yo21 | Bo11 and
A6: x= cylinder0(A2,B2,Bo21,yo21) and
A7: F1.x =cylinder0(A1,B1,Bo11,yo11) by A1;
consider Bo22 being Subset of B2,Bo12 being Subset of B1, yo12 being
Function of Bo12,A1, yo22 being Function of Bo22,A2 such that
Bo12 is finite and
Bo22 is finite and
A8: Bo12=B1 /\ Bo22 /\ (yo22"A1) and
A9: yo12=yo22 | Bo12 and
A10: x= cylinder0(A2,B2,Bo22,yo22) and
A11: F2.x =cylinder0(A1,B1,Bo12,yo12) by A2,A3;
A12: yo21 = yo22 by A6,A10,Th3;
Bo21 = Bo22 by A6,A10,Th3;
hence F1.x=F2.x by A4,A5,A7,A8,A9,A11,A12;
end;
hence F1=F2 by FUNCT_2:12;
end;
end;
definition
let A be non trivial set,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,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
proof
ex Bo be Subset of B, yo be Function of Bo,A st Bo is finite & D = {
y where y is Function of B,A : y|Bo = yo } by Th1;
hence thesis;
end;
uniqueness by Lm4;
end;
begin :: Colored Petri nets
definition
let A1,A2 be non trivial set, B1,B2 be set;
let C1,C2 be non trivial set, 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;
end;
definition
struct (PT_net_Str) Colored_PT_net_Str (# carrier, carrier' ->
set, S-T_Arcs -> Relation of the carrier,the carrier', T-S_Arcs ->
Relation of the carrier', the carrier, ColoredSet -> non empty
finite set, firing-rule -> Function #);
end;
definition
func TrivialColoredPetriNet -> Colored_PT_net_Str equals
Colored_PT_net_Str (# {{}}, {{}}, [#]({{}},{{}}), [#]({{}},
{{}}), {{}}, {} #);
coherence;
end;
registration
cluster TrivialColoredPetriNet
-> with_S-T_arc with_T-S_arc non empty non void;
coherence;
end;
registration
cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str;
existence
proof
take TrivialColoredPetriNet;
thus thesis;
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
{t0}*' = {};
end;
definition
let CPNT1 be Colored_Petri_net;
func Outbds(CPNT1) -> Subset of the carrier' of CPNT1 equals
{x where x
is transition of CPNT1 : x is outbound };
coherence
proof
{x where x is transition of CPNT1 : x is outbound } c= the carrier'
of CPNT1
proof
let z be object;
assume z in {x where x is transition of CPNT1 : x is outbound };
then ex x be transition of CPNT1 st z=x & x is outbound;
hence thesis;
end;
hence thesis;
end;
end;
definition
let CPNT be Colored_Petri_net;
attr CPNT is Colored-PT-net-like means
:Def11:
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 be non empty Subset of the
ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t}*' st (the
firing-rule of CPNT ).t is Function of thin_cylinders(CS,I), thin_cylinders(CS,
O);
end;
theorem
for CPNT be Colored_Petri_net, t being transition of CPNT st CPNT is
Colored-PT-net-like & t in dom (the firing-rule of CPNT) holds ex CS be non
empty Subset of the ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t
}*' st (the firing-rule of CPNT ).t is Function of thin_cylinders(CS,I),
thin_cylinders(CS,O);
theorem Th7:
for CPNT1,CPNT2 be Colored_Petri_net, t1 be transition of CPNT1,
t2 be 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
let CPNT1,CPNT2 be Colored_Petri_net, t1 be transition of CPNT1,t2 be
transition of CPNT2;
assume that
A1: the carrier of CPNT1 c= the carrier of CPNT2 and
A2: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 and
A3: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 and
A4: t1=t2;
thus *'{t1} c= *'{t2}
proof
let x be object;
assume
A5: x in *'{t1};
then
A6: x is place of CPNT2 by A1;
ex s be place of CPNT1 st x=s & ex f being S-T_arc of CPNT1, w being
transition of CPNT1 st w in {t1 } & f = [s,w] by A5;
then consider
f being S-T_arc of CPNT1, w being transition of CPNT1 such that
A7: w in {t2} and
A8: f = [x,w] by A4;
f is S-T_arc of CPNT2 by A2;
hence thesis by A7,A8,A6;
end;
let x be object;
assume
A9: x in {t1}*';
then
A10: x is place of CPNT2 by A1;
ex s be place of CPNT1 st x=s & ex f being T-S_arc of CPNT1, w being
transition of CPNT1 st w in { t1} & f = [w,s] by A9;
then consider
f being T-S_arc of CPNT1, w being transition of CPNT1 such that
A11: w in {t2} and
A12: f = [w,x] by A4;
f is T-S_arc of CPNT2 by A3;
hence thesis by A11,A12,A10;
end;
Lm5: for f1,f2,f3,f4,g be 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 be set st x in dom f1
holds g.x=f1.x) & (for x be set st x in dom f2 holds g.x=f2.x) & (for x be set
st x in dom f3 holds g.x=f3.x) & for x be set st x in dom f4 holds g.x=f4.x
proof
let f1,f2,f3,f4,g be Function;
assume that
A1: dom f1 /\ dom f2 = {} and
A2: dom f1 /\ dom f3 = {} and
A3: dom f1 /\ dom f4 = {} and
A4: dom f2 /\ dom f3 = {} and
A5: dom f2 /\ dom f4 = {} and
A6: dom f3 /\ dom f4 = {} and
A7: g=f1+*f2+*f3+*f4;
set f123=f1+*f2+*f3;
set f12 = f1+*f2;
thus for x be set st x in dom f1 holds g.x=f1.x
proof
let x be set;
assume
A8: x in dom f1;
then
A9: not x in dom f3 by A2,XBOOLE_0:def 4;
A10: not x in dom f2 by A1,A8,XBOOLE_0:def 4;
not x in dom f4 by A3,A8,XBOOLE_0:def 4;
hence g.x = f123.x by A7,FUNCT_4:11
.= f12.x by A9,FUNCT_4:11
.= f1.x by A10,FUNCT_4:11;
end;
thus for x be set st x in dom f2 holds g.x=f2.x
proof
let x be set;
assume
A11: x in dom f2;
then
A12: not x in dom f3 by A4,XBOOLE_0:def 4;
not x in dom f4 by A5,A11,XBOOLE_0:def 4;
hence g.x = f123.x by A7,FUNCT_4:11
.= f12.x by A12,FUNCT_4:11
.= f2.x by A11,FUNCT_4:13;
end;
thus for x be set st x in dom f3 holds g.x=f3.x
proof
let x be set;
assume
A13: x in dom f3;
then not x in dom f4 by A6,XBOOLE_0:def 4;
hence g.x = f123.x by A7,FUNCT_4:11
.= f3.x by A13,FUNCT_4:13;
end;
thus thesis by A7,FUNCT_4:13;
end;
Lm6: for A,B,C,D,X1,X2,X3,X4 be 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
let A,B,C,D,X1,X2,X3,X4 be set;
assume that
A1: A /\ B = {} and
A2: C c= A and
A3: D c= B and
A4: X1 c= A \ C and
A5: X2 c= B \ D and
A6: X3=C and
A7: X4= D;
A8: (A \ C) /\ (B \ D) c= A /\ B by XBOOLE_1:27;
X1 /\ X2 c= (A \ C) /\ (B \ D) by A4,A5,XBOOLE_1:27;
hence X1 /\ X2 = {} by A1,A8;
A9: C /\ A c= C by XBOOLE_1:17;
(A \ C) /\ C = (C /\ A) \ C by XBOOLE_1:49;
then (A \ C) /\ C= {} by A9,XBOOLE_1:37;
hence X1 /\ X3 = {} by A4,A6,XBOOLE_1:3,27;
(A \ C) /\ D = {} by A1,A3,XBOOLE_1:3,27;
hence X1 /\ X4 = {} by A4,A7,XBOOLE_1:3,27;
(B \ D) /\ C = {} by A1,A2,XBOOLE_1:3,27;
hence X2 /\ X3 = {} by A5,A6,XBOOLE_1:3,27;
A10: B /\ D c= D by XBOOLE_1:17;
(B \ D) /\ D = (B /\ D) \ D by XBOOLE_1:49;
then (B \ D) /\ D= {} by A10,XBOOLE_1:37;
hence X2 /\ X4 = {} by A5,A7,XBOOLE_1:3,27;
thus thesis by A1,A2,A3,A6,A7,XBOOLE_1:3,27;
end;
registration
cluster strict Colored-PT-net-like for Colored_Petri_net;
existence
proof
set PLA={0};
set a = the set;
set TRA={a};
set TSA= [:TRA,PLA:];
TSA c= TSA;
then reconsider TSA as non empty Relation of TRA,PLA;
set STA = [:PLA,TRA:];
STA c= STA;
then reconsider STA as non empty Relation of PLA,TRA;
set CS = {a,a,a};
set fa = the Function of thin_cylinders(CS,{0}), thin_cylinders(CS,{0});
set f= ({a} --> fa);
set CPNT = Colored_PT_net_Str(# PLA,TRA,STA,TSA, CS,f #);
A1: CPNT is with_S-T_arc;
CPNT is with_T-S_arc;
then reconsider CPNT as Colored_Petri_net by A1;
take CPNT;
A2: now
CS c= CS;
then reconsider CS1= CS as non empty Subset of the ColoredSet of CPNT;
let t be transition of CPNT;
assume t in dom (the firing-rule of CPNT);
A3: t= a by TARSKI:def 1;
A4: a in TRA by TARSKI:def 1;
A5: 0 in PLA by TARSKI:def 1;
then [a,0] in TSA by A4,ZFMISC_1:87;
then 0 in {t} *' by A3,PETRI:8;
then reconsider O = {0} as Subset of {t} *' by ZFMISC_1:31;
[0,a] in STA by A5,A4,ZFMISC_1:87;
then 0 in *'{t} by A3,PETRI:6;
then reconsider I = {0} as Subset of *'{t} by ZFMISC_1:31;
A6: fa is Function of thin_cylinders(CS1,I), thin_cylinders(CS1,O );
f.t =fa by FUNCOP_1:7;
hence ex CS1 be non empty Subset of the ColoredSet of CPNT, I be Subset
of *'{t}, O be Subset of {t}*' st (the firing-rule of CPNT ).t is Function of
thin_cylinders(CS1,I), thin_cylinders(CS1,O ) by A6;
end;
A7: dom f = {a} by FUNCOP_1:13;
now
reconsider a1=a as transition of CPNT by TARSKI:def 1;
let x be object;
0 in PLA by TARSKI:def 1;
then [a1,0] in TSA by ZFMISC_1:87;
then
A8: not {a1}*' = {} by PETRI:8;
A9: not a1 in Outbds(CPNT)
proof
assume a1 in Outbds(CPNT);
then ex x be transition of CPNT st a1=x & x is outbound;
hence contradiction by A8;
end;
assume x in dom (the firing-rule of CPNT);
then x=a by A7,TARSKI:def 1;
hence x in (the carrier' of CPNT) \ Outbds(CPNT) by A9,XBOOLE_0:def 5;
end;
then dom (the firing-rule of CPNT) c= (the carrier' of CPNT) \ Outbds(
CPNT);
hence thesis by A2;
end;
end;
definition
mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;
end;
begin :: Outbound transitions of CPNT
definition
let CPNT1, CPNT2 be Colored_Petri_net;
pred CPNT1 misses CPNT2 means
(the carrier of CPNT1) /\ (the carrier
of CPNT2 ) = {} & (the carrier' of CPNT1) /\ (the carrier' of CPNT2) = {};
symmetry;
end;
begin :: Connecting mapping for CPNT1,CPNT2
definition
let CPNT1 be Colored_Petri_net;
let CPNT2 be Colored_Petri_net;
mode connecting-mapping of CPNT1,CPNT2 -> set means
:Def13:
ex O12 be Function of
Outbds(CPNT1), the carrier of CPNT2, O21 be Function of Outbds(CPNT2), the
carrier of CPNT1 st it=[O12,O21];
correctness
proof
set O12 = the Function of Outbds(CPNT1), the carrier of CPNT2,O21 =the
Function of Outbds(CPNT2), the carrier of CPNT1;
set Z = [O12,O21];
take Z;
thus thesis;
end;
end;
begin :: Connecting firing rule for CPNT1,CPNT2
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:
ex q12,q21 be
Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
dom q12=Outbds(
CPNT1) & dom q21=Outbds(CPNT2) & ( for t01 be 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
be 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
proof
set L2=bool PFuncs(the carrier of CPNT1, the ColoredSet of CPNT2);
set L1=bool PFuncs(the carrier of CPNT2, the ColoredSet of CPNT2);
set K2=bool PFuncs(the carrier of CPNT2, the ColoredSet of CPNT1);
set K1=bool PFuncs(the carrier of CPNT1, the ColoredSet of CPNT1);
set TO2 = Outbds(CPNT2);
set TO1 = Outbds(CPNT1);
set Y1= PFuncs(K1,K2);
set Y2= PFuncs(L1,L2);
consider O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 such that
A1: O = [O12,O21] by Def13;
defpred R[object,object] means
ex t02 be transition of CPNT2 st $1=t02 & $2 is
Function of thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders
( the ColoredSet of CPNT2, Im(O21,t02));
defpred P[object,object] means
ex t01 be transition of CPNT1 st $1=t01 & $2 is
Function of thin_cylinders (the ColoredSet of CPNT1, *'{t01}), thin_cylinders (
the ColoredSet of CPNT1, Im(O12,t01) );
A2: for x be object st x in TO1 ex y be object st y in Y1 & P[x,y]
proof
let x be object;
assume x in TO1;
then consider t01 be transition of CPNT1 such that
A3: x=t01 and
t01 is outbound;
set t2=Im(O12,t01);
set t1=*'{t01};
set y = the Function of thin_cylinders ( the ColoredSet of CPNT1, t1),
thin_cylinders ( the ColoredSet of CPNT1, t2);
take y;
set H1= thin_cylinders ( the ColoredSet of CPNT1, t1);
set H2= thin_cylinders ( the ColoredSet of CPNT1, t2);
A4: Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:72;
A5: H2 c= bool PFuncs(the carrier of CPNT2, the ColoredSet of CPNT1) by Lm1;
H1 c= bool PFuncs(the carrier of CPNT1, the ColoredSet of CPNT1) by Lm1;
then
A6: PFuncs(H1,H2) c= PFuncs(K1,K2) by A5,PARTFUN1:50;
y in Funcs(H1,H2) by FUNCT_2:8;
then y in PFuncs(H1,H2) by A4;
hence thesis by A3,A6;
end;
consider q12 be Function of TO1,Y1 such that
A7: for x be object st x in TO1 holds P[x,q12.x] from FUNCT_2:sch 1(A2);
A8: now
let tt01 be transition of CPNT1;
assume tt01 is outbound;
then tt01 in TO1;
then
ex t01 be transition of CPNT1 st tt01=t01 & q12.tt01 is Function of
thin_cylinders ( the ColoredSet of CPNT1, *'{t01}), thin_cylinders ( the
ColoredSet of CPNT1, Im(O12,t01) ) by A7;
hence q12.tt01 is Function of thin_cylinders ( the ColoredSet of CPNT1,
*'{tt01}), thin_cylinders ( the ColoredSet of CPNT1, Im(O12,tt01) );
end;
A9: for x be object st x in TO2 ex y be object st y in Y2 & R[x,y]
proof
let x be object;
assume x in TO2;
then consider t02 be transition of CPNT2 such that
A10: x=t02 and
t02 is outbound;
set t2= Im(O21,t02);
set t1=*'{t02};
set y = the Function of thin_cylinders ( the ColoredSet of CPNT2, t1),
thin_cylinders ( the ColoredSet of CPNT2, t2);
take y;
set H1= thin_cylinders ( the ColoredSet of CPNT2, t1);
set H2= thin_cylinders ( the ColoredSet of CPNT2, t2);
A11: Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:72;
A12: H2 c= bool PFuncs(the carrier of CPNT1, the ColoredSet of CPNT2) by Lm1;
H1 c= bool PFuncs(the carrier of CPNT2, the ColoredSet of CPNT2) by Lm1;
then
A13: PFuncs(H1,H2) c= PFuncs(L1,L2) by A12,PARTFUN1:50;
y in Funcs(H1,H2) by FUNCT_2:8;
then y in PFuncs(H1,H2) by A11;
hence thesis by A10,A13;
end;
consider q21 be Function of TO2,Y2 such that
A14: for x be object st x in TO2 holds R[x,q21.x] from FUNCT_2:sch 1(A9);
A15: now
let tt02 be transition of CPNT2;
assume tt02 is outbound;
then tt02 in TO2;
then
ex t02 be transition of CPNT2 st tt02=t02 & q21.tt02 is Function of
thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders ( the
ColoredSet of CPNT2, Im(O21,t02)) by A14;
hence q21.tt02 is Function of thin_cylinders ( the ColoredSet of CPNT2,
*'{tt02}), thin_cylinders ( the ColoredSet of CPNT2, Im(O21,tt02));
end;
take [q12,q21];
A16: dom q21=Outbds(CPNT2) by FUNCT_2:def 1;
dom q12=Outbds(CPNT1) by FUNCT_2:def 1;
hence thesis by A1,A8,A15,A16;
end;
end;
begin :: Synthesis of CPNT1,CPNT2
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
be Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
dom q12=Outbds(
CPNT1) & dom q21=Outbds(CPNT2) & ( for t01 be 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
be 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
proof
reconsider CS12 = (the ColoredSet of CPNT1) \/ (the ColoredSet of CPNT2)
as non empty finite set;
reconsider T12 = (the carrier' of CPNT1) \/ (the carrier' of CPNT2)
as non empty set;
reconsider P12 = (the carrier of CPNT1) \/ (the carrier of CPNT2) as non
empty set;
A2: (the carrier' of CPNT1) c= T12 by XBOOLE_1:7;
(the carrier of CPNT1) c= P12 by XBOOLE_1:7;
then reconsider E1=(the S-T_Arcs of CPNT1) as Relation of P12,T12 by A2,
RELSET_1:7;
A3: (the carrier of CPNT2) c= P12 by XBOOLE_1:7;
(the carrier' of CPNT2) c= T12 by XBOOLE_1:7;
then reconsider E22=(the T-S_Arcs of CPNT2) as Relation of T12,P12 by A3,
RELSET_1:7;
set R1=the firing-rule of CPNT1;
A4: (the carrier' of CPNT2) c= T12 by XBOOLE_1:7;
(the carrier of CPNT2) c= P12 by XBOOLE_1:7;
then reconsider E2=(the S-T_Arcs of CPNT2) as Relation of P12,T12 by A4,
RELSET_1:7;
set R2=the firing-rule of CPNT2;
A5: (the carrier of CPNT1) c= P12 by XBOOLE_1:7;
(the carrier' of CPNT1) c= T12 by XBOOLE_1:7;
then reconsider E21=(the T-S_Arcs of CPNT1) as Relation of T12,P12 by A5,
RELSET_1:7;
A6: (the T-S_Arcs of CPNT1) c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs
of CPNT2) by XBOOLE_1:7;
E1 \/ E2 is Relation of P12,T12;
then reconsider
ST12= (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) as non
empty Relation of P12,T12;
A7: (the T-S_Arcs of CPNT2) c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs
of CPNT2) by XBOOLE_1:7;
E21 \/ E22 is Relation of T12,P12;
then reconsider
TTS12= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) as
non empty Relation of T12,P12;
consider q12,q21 be Function, O12 be Function of Outbds(CPNT1), the carrier
of CPNT2, O21 be Function of Outbds(CPNT2), the carrier of CPNT1 such that
A8: O=[O12,O21] and
A9: dom q12=Outbds(CPNT1) and
A10: dom q21=Outbds(CPNT2) and
A11: for t01 be 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) ) and
A12: for t02 be 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) ) and
A13: q=[q12,q21] by Def14;
A14: dom (the firing-rule of CPNT2) c= (the carrier' of CPNT2) \ (dom
q21) by A10,Def11;
(the carrier' of CPNT2) c= T12 by XBOOLE_1:7;
then
A15: Outbds(CPNT2) c= T12;
(the carrier' of CPNT1) c= T12 by XBOOLE_1:7;
then
A16: Outbds(CPNT1) c= T12;
A17: (the carrier' of CPNT1) /\ (the carrier' of CPNT2) = {} by A1;
A18: dom (the firing-rule of CPNT1) c= (the carrier' of CPNT1) \ (dom
q12) by A9,Def11;
then
A19: dom (the firing-rule of CPNT1) /\ dom (the firing-rule of CPNT2) = {}
by A9,A10,A17,A14,Lm6;
A20: dom (the firing-rule of CPNT2) /\ dom q21 = {} by A9,A10,A17,A18,A14,Lm6;
A21: dom (the firing-rule of CPNT2) /\ dom q12 = {} by A9,A10,A17,A18,A14,Lm6;
A22: dom q12 /\ dom q21 ={} by A9,A10,A17,A18,A14,Lm6;
A23: dom (the firing-rule of CPNT1) /\ dom q21 = {} by A9,A10,A17,A18,A14,Lm6;
A24: dom (the firing-rule of CPNT1) /\ dom q12 = {} by A9,A10,A17,A18,A14,Lm6;
the carrier of CPNT1 c= P12 by XBOOLE_1:7;
then reconsider E32=O21 as Relation of T12,P12 by A15,RELSET_1:7;
the carrier of CPNT2 c= P12 by XBOOLE_1:7;
then reconsider E31=O12 as Relation of T12,P12 by A16,RELSET_1:7;
set R4=q21;
set R3=q12;
set CR12= (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12
+* q21;
reconsider TS12= TTS12 \/ (E31 \/ E32) as non empty Relation of T12,P12;
set CPNT12=Colored_PT_net_Str(# P12,T12, ST12,TS12,CS12,CR12 #);
A25: CPNT12 is with_S-T_arc;
CPNT12 is with_T-S_arc;
then reconsider CPNT12 as Colored_Petri_net by A25;
A26: the carrier of CPNT1 c= the carrier of CPNT12 by XBOOLE_1:7;
A27: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) c= the T-S_Arcs of
CPNT12 by XBOOLE_1:7;
then
A28: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12 by A6;
A29: the carrier of CPNT2 c= the carrier of CPNT12 by XBOOLE_1:7;
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) c= the T-S_Arcs of
CPNT12 by XBOOLE_1:7;
then
A30: the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12 by A7;
A31: the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
A32: now
let x be set;
assume x in dom CR12;
then x in dom ( R1 +* R2 +* R3) or x in dom R4 by FUNCT_4:12;
then x in dom ( R1 +* R2 ) or x in dom R3 or x in dom R4 by FUNCT_4:12;
hence x in dom R1 or x in dom R2 or x in dom R3 or x in dom R4 by
FUNCT_4:12;
end;
A33: for t being transition of CPNT12 st t in dom (the firing-rule of
CPNT12) holds ex CS be non empty Subset of the ColoredSet of CPNT12, I be
Subset of *'{t}, O be Subset of {t}*' st (the firing-rule of CPNT12 ).t is
Function of thin_cylinders(CS,I), thin_cylinders(CS,O)
proof
let t be transition of CPNT12;
assume
A34: t in dom (the firing-rule of CPNT12);
now
per cases by A32,A34;
suppose
A35: t in dom the firing-rule of CPNT1;
dom ( the firing-rule of CPNT1) c= (the carrier' of CPNT1) \
Outbds(CPNT1) by Def11;
then reconsider t1 =t as transition of CPNT1 by A35,TARSKI:def 3;
consider CS1 be non empty Subset of the ColoredSet of CPNT1, I1 be
Subset of *'{t1}, O1 be Subset of {t1}*' such that
A36: (the firing-rule of CPNT1).t1 is Function of thin_cylinders
(CS1,I1), thin_cylinders(CS1,O1) by A35,Def11;
*'{t1} c= *'{t} by A26,A27,A28,Th7;
then reconsider I =I1 as Subset of *'{t} by XBOOLE_1:1;
the ColoredSet of CPNT1 c= the ColoredSet of CPNT12 by XBOOLE_1:7;
then reconsider
CS = CS1 as non empty Subset of the ColoredSet of CPNT12
by XBOOLE_1:1;
{t1}*' c= {t}*' by A26,A27,A28,Th7;
then reconsider O =O1 as Subset of {t}*' by XBOOLE_1:1;
(the firing-rule of CPNT12).t is Function of thin_cylinders(CS,
I), thin_cylinders(CS,O) by A19,A24,A23,A21,A20,A22,A35,A36,Lm5;
hence thesis;
end;
suppose
A37: t in dom ( the firing-rule of CPNT2);
dom ( the firing-rule of CPNT2) c= (the carrier' of CPNT2) \
Outbds(CPNT2) by Def11;
then reconsider t1 = t as transition of CPNT2 by A37,TARSKI:def 3;
consider CS1 be non empty Subset of the ColoredSet of CPNT2, I1 be
Subset of *'{t1}, O1 be Subset of {t1}*' such that
A38: (the firing-rule of CPNT2).t1 is Function of thin_cylinders
(CS1,I1), thin_cylinders(CS1,O1) by A37,Def11;
*'{t1} c= *'{t} by A29,A31,A30,Th7;
then reconsider I =I1 as Subset of *'{t} by XBOOLE_1:1;
the ColoredSet of CPNT2 c= the ColoredSet of CPNT12 by XBOOLE_1:7;
then reconsider
CS = CS1 as non empty Subset of the ColoredSet of CPNT12
by XBOOLE_1:1;
{t1}*' c= {t}*' by A29,A31,A30,Th7;
then reconsider O =O1 as Subset of {t}*' by XBOOLE_1:1;
(the firing-rule of CPNT12).t is Function of thin_cylinders(CS,
I), thin_cylinders(CS,O) by A19,A24,A23,A21,A20,A22,A37,A38,Lm5;
hence thesis;
end;
suppose
A39: t in dom (q12);
then reconsider t1 =t as transition of CPNT1 by A9;
reconsider I =*'{t1} as Subset of *'{t} by A26,A27,A28,Th7;
reconsider CS = the ColoredSet of CPNT1 as non empty Subset of the
ColoredSet of CPNT12 by XBOOLE_1:7;
Im(O12,t1) c= {t}*'
proof
let x be object;
A40: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
assume
A41: x in Im(O12,t1);
then reconsider s = x as place of CPNT2;
A42: [t1,s] in O12 by A41,RELSET_2:9;
O12 c= E31 \/ E32 by XBOOLE_1:7;
then O12 c= the T-S_Arcs of CPNT12 by A40;
then reconsider f= [t,s] as T-S_arc of CPNT12 by A42;
A43: the carrier of CPNT2 c= (the carrier of CPNT1) \/ (the carrier of
CPNT2) by XBOOLE_1:7;
A44: f=[t,s];
A45: t in {t} by TARSKI:def 1;
s in the carrier of CPNT2;
hence thesis by A43,A45,A44;
end;
then reconsider O = Im(O12,t1) as Subset of {t}*';
ex x1 be transition of CPNT1 st t1=x1 & x1 is outbound by A9,A39;
then
q12.t1 is Function of thin_cylinders ( the ColoredSet of CPNT1,
*'{t1}), thin_cylinders ( the ColoredSet of CPNT1, Im(O12,t1) ) by A11;
then
(the firing-rule of CPNT12).t is Function of thin_cylinders(CS,
I), thin_cylinders(CS,O) by A19,A24,A23,A21,A20,A22,A39,Lm5;
hence thesis;
end;
suppose
A46: t in dom (q21);
then reconsider t1 = t as transition of CPNT2 by A10;
reconsider I =*'{t1} as Subset of *'{t} by A29,A31,A30,Th7;
reconsider CS = the ColoredSet of CPNT2 as non empty Subset of the
ColoredSet of CPNT12 by XBOOLE_1:7;
Im(O21,t1) c= {t}*'
proof
let x be object;
A47: O21 c= E31 \/ E32 by XBOOLE_1:7;
assume
A48: x in Im(O21,t1);
then reconsider s=x as place of CPNT1;
A49: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
[t1,s] in O21 by A48,RELSET_2:9;
then reconsider f= [t,s] as T-S_arc of CPNT12 by A47,A49;
A50: the carrier of CPNT1 c= (the carrier of CPNT1) \/ (the carrier
of CPNT2) by XBOOLE_1:7;
A51: f=[t,s];
A52: t in {t} by TARSKI:def 1;
s in the carrier of CPNT1;
hence thesis by A50,A52,A51;
end;
then reconsider O = Im(O21,t1) as Subset of {t}*';
ex x1 be transition of CPNT2 st t1=x1 & x1 is outbound by A10,A46;
then q21.t1 is Function of thin_cylinders (the ColoredSet of CPNT2,
*'{t1}), thin_cylinders (the ColoredSet of CPNT2, Im(O21,t1) ) by A12;
then (the firing-rule of CPNT12).t is Function of thin_cylinders(CS
,I), thin_cylinders(CS,O) by A19,A24,A23,A21,A20,A22,A46,Lm5;
hence thesis;
end;
end;
hence thesis;
end;
A53: TS12= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/O21
by XBOOLE_1:4;
A54: now
let x be object;
dom ( the firing-rule of CPNT1) c= (the carrier' of CPNT1) \
Outbds(CPNT1) by Def11;
then
A55: dom ( the firing-rule of CPNT1) c= the carrier' of CPNT1 by XBOOLE_1:1;
dom ( the firing-rule of CPNT2) c= (the carrier' of CPNT2) \
Outbds(CPNT2) by Def11;
then
A56: dom ( the firing-rule of CPNT2) c= the carrier' of CPNT2 by XBOOLE_1:1;
assume x in dom CR12;
then x in dom R1 or x in dom R2 or x in dom R3 or x in dom R4 by A32;
hence
x in (the carrier' of CPNT1) \/ (the carrier' of CPNT2) by A9,A10,A55,A56
,XBOOLE_0:def 3;
end;
then
A57: dom (the firing-rule of CPNT12) c= the carrier' of CPNT12;
dom (the firing-rule of CPNT12) c= (the carrier' of CPNT12) \
Outbds(CPNT12)
proof
set RR4=q21;
set RR3=q12;
set RR2=the firing-rule of CPNT2;
set RR1=the firing-rule of CPNT1;
let x be object;
assume
A58: x in dom (the firing-rule of CPNT12);
then reconsider t=x as transition of CPNT12 by A54;
now
per cases by A32,A58;
suppose
A59: t in dom RR1;
A60: dom ( the firing-rule of CPNT1) c= (the carrier' of CPNT1)
\ Outbds(CPNT1) by Def11;
then reconsider t1 =t as transition of CPNT1 by A59,XBOOLE_0:def 5;
not t in Outbds(CPNT1) by A59,A60,XBOOLE_0:def 5;
then not t1 is outbound;
then {t1}*' <> {};
then
A61: ex g be object st g in {t1}*' by XBOOLE_0:def 1;
{t1}*' c= {t}*' by A26,A27,A28,Th7;
then not ex w be transition of CPNT12 st t=w & w is outbound by A61;
hence not x in Outbds(CPNT12);
end;
suppose
A62: t in dom RR2;
A63: dom ( the firing-rule of CPNT2) c= (the carrier' of CPNT2) \
Outbds(CPNT2) by Def11;
then reconsider t1 =t as transition of CPNT2 by A62,XBOOLE_0:def 5;
not t in Outbds(CPNT2) by A62,A63,XBOOLE_0:def 5;
then not t1 is outbound;
then {t1}*' <> {};
then
A64: ex g be object st g in {t1}*' by XBOOLE_0:def 1;
{t1}*' c= {t}*' by A29,A31,A30,Th7;
then not (ex w be transition of CPNT12 st t=w & w is outbound ) by
A64;
hence not x in Outbds(CPNT12);
end;
suppose
t in dom RR3;
then t in dom O12 by A9,FUNCT_2:def 1;
then consider s be object such that
A65: [t,s] in O12 by XTUPLE_0:def 12;
reconsider s as place of CPNT2 by A65,ZFMISC_1:87;
A66: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
O12 c= E31 \/ E32 by XBOOLE_1:7;
then O12 c= the T-S_Arcs of CPNT12 by A66;
then reconsider f= [t,s] as T-S_arc of CPNT12 by A65;
A67: the carrier of CPNT2 c= (the carrier of CPNT1) \/ (the carrier of
CPNT2) by XBOOLE_1:7;
A68: f=[t,s];
A69: t in {t} by TARSKI:def 1;
s in the carrier of CPNT2;
then s in {t}*' by A67,A69,A68;
then not (ex w be transition of CPNT12 st t=w & w is outbound);
hence not x in Outbds(CPNT12);
end;
suppose
t in dom RR4;
then t in dom O21 by A10,FUNCT_2:def 1;
then consider s be object such that
A70: [t,s] in O21 by XTUPLE_0:def 12;
reconsider s as place of CPNT1 by A70,ZFMISC_1:87;
A71: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
O21 c= E31 \/ E32 by XBOOLE_1:7;
then O21 c= the T-S_Arcs of CPNT12 by A71;
then reconsider f= [t,s] as T-S_arc of CPNT12 by A70;
A72: the carrier of CPNT1 c= (the carrier of CPNT1) \/ (the carrier of
CPNT2) by XBOOLE_1:7;
A73: f=[t,s];
A74: t in {t} by TARSKI:def 1;
s in the carrier of CPNT1;
then s in {t}*' by A72,A74,A73;
then not (ex w be transition of CPNT12 st t=w & w is outbound);
hence not x in Outbds(CPNT12);
end;
end;
hence thesis by A57,A58,XBOOLE_0:def 5;
end;
then CPNT12 is Colored-PT-net-like by A33;
hence thesis by A8,A9,A10,A11,A12,A13,A53;
end;
uniqueness
proof
let CA,CB be strict Colored-PT-net;
assume ex q12A,q21A be Function, O12A be Function of Outbds(CPNT1), the
carrier of CPNT2, O21A be Function of Outbds(CPNT2), the carrier of CPNT1
st O=[
O12A,O21A] &dom q12A=Outbds(CPNT1) & dom q21A=Outbds(CPNT2) & ( for t01 be
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 be transition of CPNT2 st t02
is outbound holds q21A.t02 is Function of thin_cylinders ( the ColoredSet of
CPNT2, *'{t02}), thin_cylinders ( the ColoredSet of CPNT2, Im(O21A,t02) ) ) & q
=[q12A,q21A] & the carrier of CA
= (the carrier of CPNT1) \/ (the carrier of CPNT2
) & the carrier' of CA = (the carrier' of CPNT1) \/ (the carrier' of
CPNT2) & the S-T_Arcs of CA = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2
) & the T-S_Arcs of CA = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/
O12A \/ O21A & the ColoredSet of CA = (the ColoredSet of CPNT1) \/ (the
ColoredSet of CPNT2) & the firing-rule of CA = (the firing-rule of CPNT1) +* (
the firing-rule of CPNT2) +* q12A +* q21A;
then consider
q12A,q21A be Function, O12A be Function of Outbds(CPNT1), the
carrier of CPNT2, O21A be Function of Outbds(CPNT2), the carrier of CPNT1 such
that
A75: O=[O12A,O21A] and
dom q12A=Outbds(CPNT1) and
dom q21A=Outbds(CPNT2) and
for t01 be transition of CPNT1 st t01 is outbound holds q12A.t01 is
Function of thin_cylinders ( the ColoredSet of CPNT1, *'{t01}), thin_cylinders
( the ColoredSet of CPNT1, Im(O12A,t01) ) and
for t02 be transition of CPNT2 st t02 is outbound holds q21A.t02 is
Function of thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders
( the ColoredSet of CPNT2, Im(O21A,t02)) and
A76: q=[q12A,q21A] and
A77: the carrier of CA = (the carrier of CPNT1) \/ (the carrier of CPNT2 ) and
A78: the carrier' of CA = (the carrier' of CPNT1) \/ (the
carrier' of CPNT2) and
A79: the S-T_Arcs of CA = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of
CPNT2) and
A80: the T-S_Arcs of CA = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of
CPNT2) \/ O12A \/O21A and
A81: the ColoredSet of CA = (the ColoredSet of CPNT1) \/ (the
ColoredSet of CPNT2) and
A82: the firing-rule of CA = (the firing-rule of CPNT1) +* (the
firing-rule of CPNT2) +* q12A +* q21A;
assume ex q12B,q21B be Function, O12B be Function of Outbds(CPNT1), the
carrier of CPNT2, O21B be Function of Outbds(CPNT2), the carrier of CPNT1
st O=[
O12B,O21B] & dom q12B=Outbds(CPNT1) & dom q21B=Outbds(CPNT2) & ( for t01 be
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 be transition of CPNT2 st t02
is outbound holds q21B.t02 is Function of thin_cylinders ( the ColoredSet of
CPNT2, *'{t02}), thin_cylinders ( the ColoredSet of CPNT2, Im(O21B,t02) ) ) & q
=[q12B,q21B] & the carrier of CB
= (the carrier of CPNT1) \/ (the carrier of CPNT2
) & the carrier' of CB = (the carrier' of CPNT1) \/ (the carrier' of
CPNT2) & the S-T_Arcs of CB = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2
) & the T-S_Arcs of CB = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/
O12B \/ O21B & the ColoredSet of CB = (the ColoredSet of CPNT1) \/ (the
ColoredSet of CPNT2) & the firing-rule of CB = (the firing-rule of CPNT1) +* (
the firing-rule of CPNT2) +* q12B +* q21B;
then consider
q12B,q21B be Function, O12B be Function of Outbds(CPNT1), the
carrier of CPNT2, O21B be Function of Outbds(CPNT2), the carrier of CPNT1 such
that
A83: O=[O12B,O21B] and
dom q12B=Outbds(CPNT1) and
dom q21B=Outbds(CPNT2) and
for t01 be transition of CPNT1 st t01 is outbound holds q12B.t01 is
Function of thin_cylinders ( the ColoredSet of CPNT1, *'{t01}), thin_cylinders
( the ColoredSet of CPNT1, Im(O12B,t01)) and
for t02 be transition of CPNT2 st t02 is outbound holds q21B.t02 is
Function of thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders
( the ColoredSet of CPNT2, Im(O21B,t02)) and
A84: q=[q12B,q21B] and
A85: the carrier of CB = (the carrier of CPNT1) \/ (the carrier of CPNT2 ) and
A86: the carrier' of CB = (the carrier' of CPNT1) \/ (the
carrier' of CPNT2) and
A87: the S-T_Arcs of CB = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of
CPNT2) and
A88: the T-S_Arcs of CB = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of
CPNT2) \/ O12B \/O21B and
A89: the ColoredSet of CB = (the ColoredSet of CPNT1) \/ (the
ColoredSet of CPNT2) and
A90: the firing-rule of CB = (the firing-rule of CPNT1) +* (the
firing-rule of CPNT2) +* q12B +* q21B;
A91: q21A =q21B by A76,A84,XTUPLE_0:1;
A92: O12A=O12B by A75,A83,XTUPLE_0:1;
q12A=q12B by A76,A84,XTUPLE_0:1;
hence
thesis by A75,A77,A78,A79,A80,A81,A82,A83,A85,A86,A87,A88,A89,A90,A91,A92,
XTUPLE_0:1;
end;
end;