:: Cell Petri Net Concepts
:: by Mitsuru Jitsukawa , Pauline N. Kawamoto , Yasunari Shidama and Yatsuka Nakamura
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies RELAT_1, NET_1, ARYTM_3, BOOLE, PETRI, PETRI_2, FUNCT_1, ARYTM,
FINSET_1, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, SETFAM_1, COMPLEX1,
REALSET1;
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, CARD_1, NUMBERS;
constructors RELAT_1, ENUMSET1, RELSET_1, DOMAIN_1, MEMBERED, XBOOLE_0,
VALUED_1, PETRI, FUNCT_2, PARTFUN1, RELSET_2, SEQ_1, FUNCOP_1, ORDINAL1,
FINSET_1, NAT_1, FUNCT_4, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1,
WELLORD2;
registrations SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, PARTFUN1, RELSET_1,
XBOOLE_0, MEMBERED, FUNCOP_1, TREES_2, VALUED_1, XXREAL_0, XREAL_0,
REAL_1, ZFMISC_1, NAT_1, FUNCT_2, FUNCT_4, FINSET_1, PETRI, REALSET1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions ENUMSET1, TARSKI, XBOOLE_0, PETRI, FUNCT_2, FUNCT_4, PARTFUN1,
ORDINAL1, FUNCOP_1, WELLORD2, RELAT_1, FINSET_1, RELSET_1, CARD_1;
theorems RELSET_1, PARTFUN1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, PETRI,
FUNCT_1, FUNCT_2, XBOOLE_1, FUNCT_4, FUNCOP_1, RELSET_2;
schemes FUNCT_2;
begin :: Preliminaries: thin cylinder, locus
reserve PTN for PT_net_Str;
reserve y for Function;
reserve z for set;
definition
let A be non empty set, B be set;
let Bo be set, yo be Function of Bo,A;
assume
AS: Bo c= B;
func cylinder0(A,B,Bo,yo) -> non empty Subset of Funcs(B,A) equals
:DefX01:
{ 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 };
A3: now let z be set;
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:11;
end;
now per cases;
suppose C1: Bo = {};
consider f being Function of B,A;
f|{} = {} .= yo by C1;
then f in D by C1;
hence D is non empty;
end;
suppose Bo <> {}; then
consider b0 be set such that
D2: b0 in Bo by XBOOLE_0:def 1;
set f = (B --> yo.b0) +* yo;
C: rng f c= rng(B --> yo.b0) \/ rng yo by FUNCT_4:18;
E: rng(B --> yo.b0) c= {yo.b0} by FUNCOP_1:19;
B: dom yo = Bo by FUNCT_2:def 1;
yo.b0 in A by D2,FUNCT_2:7;
then {yo.b0} c= A by ZFMISC_1:37;
then
D: rng(B --> yo.b0) c= A by E,XBOOLE_1:1;
rng yo c= A by RELSET_1:12;
then
A: rng(B --> yo.b0) \/ rng yo c= A by D,XBOOLE_1:8;
dom f = dom(B --> yo.b0) \/ Bo by B,FUNCT_4:def 1
.= B \/ Bo by FUNCOP_1:19
.= B by AS,XBOOLE_1:12;
then reconsider f as Function of B,A by A,FUNCT_2:4,C,XBOOLE_1:1;
f|Bo = yo by B,FUNCT_4:24;
then f in D;
hence D is non empty;
end;
end;
hence thesis by A3,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
:Def21:
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={};
A2: Bo is Subset of B & Bo is finite by XBOOLE_1:2;
consider yo being Function of Bo,A;
take D= cylinder0(A,B,Bo,yo);
thus thesis by A2;
end;
end;
theorem LM1:
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 &
D = cylinder0(A,B,Bo,yo) by Def21;
D = { y where y is Function of B,A : y|Bo = yo } by DefX01,A1;
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;
assume AS: A1 c= A2;
consider Bo being Subset of B,yo1 being Function of Bo,A1 such that
P1: Bo is finite &
D1 = { y where y is Function of B,A1: y|Bo = yo1 } by LM1;
reconsider yo2=yo1 as Function of Bo,A2 by AS, FUNCT_2:9;
set D2= { y where y is Function of B,A2: y|Bo = yo2 };
S1: now let x be set;
assume x in D1;
then consider y1 be Function of B,A1 such that
P4: x=y1 & y1|Bo = yo1 by P1;
reconsider y2=y1 as Function of B,A2 by FUNCT_2:9,AS;
x=y1 & y2|Bo = yo1 by P4;
hence x in D2;
end;
D2= cylinder0(A2,B,Bo,yo2) by DefX01;
then reconsider D2 as thin_cylinder of A2,B by P1,Def21;
take D2;
thus thesis by S1,TARSKI:def 3;
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
consider F be thin_cylinder of A,B;
P2: F in {D where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
now let z be set;
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;
hence thesis by P2,TARSKI:def 3;
end;
end;
LmThin:
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 AS: B c= C;
let x be set;
assume x in thin_cylinders(A,B);
then consider D be Subset of Funcs(B,A) such that
P1: x=D & D is thin_cylinder of A,B;
P2: D in bool Funcs(B,A);
P3: Funcs(B,A) c= PFuncs(B,A) by FUNCT_2:141;
PFuncs(B,A) c= PFuncs(C,A) by AS,PARTFUN1:128;
then
Funcs(B,A) c= PFuncs(C,A) by XBOOLE_1:1,P3;
then
bool Funcs(B,A) c= bool PFuncs(C,A) by ZFMISC_1:79;
hence x in bool PFuncs(C,A) by P1,P2;
end;
Lm11:
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;
assume not Bo2 c= Bo1;
then consider x0 be set such that
D1: x0 in Bo2 & not x0 in Bo1 by TARSKI:def 3;
ex y0 be set st y0 in A & y0 <> yo2.x0
proof
consider x,y be set such that
D21: x in A & y in A & x <> y by ZFMISC_1:def 10;
per cases;
suppose C1:yo2.x0 = x;
take y;
thus thesis by C1,D21;
end;
suppose C2:yo2.x0 <> x;
take x;
thus thesis by C2,D21;
end;
end;
then consider y0 be set such that
D2: y0 in A & y0 <> yo2.x0;
defpred C[set] means $1 in Bo1;
deffunc F(set) = yo1.$1;
deffunc G(set) = y0;
D3: for x be set st x in B holds
(C[ x] implies F(x) in A) & (not C[ x] implies G(x) in A)
by D2,FUNCT_2:7;
consider f be Function of B, A such that
D4: for x be set 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(D3);
P1: dom yo1 = Bo1 by FUNCT_2:def 1
.= B /\ Bo1 by XBOOLE_1:28
.= dom f /\ Bo1 by FUNCT_2:def 1;
now let z be set;
assume z in dom yo1;
then z in Bo1;
hence yo1.z = f.z by D4;
end; then
P2:f|Bo1 = yo1 by P1, FUNCT_1:68;
P3: x0 in dom yo2 by D1,FUNCT_2:def 1;
f.x0 <> yo2.x0 by D2,D4,D1; then
f|Bo2 <> yo2 by P3, FUNCT_1:68;
hence thesis by P2;
end;
Lm12:
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 Bo1 <> Bo2 & Bo2 c= Bo1; then
Bo2 c< Bo1 by XBOOLE_0:def 8; then
consider x0 be set such that
D1: x0 in Bo1 & not x0 in Bo2 by XBOOLE_0:6;
ex y0 be set st
y0 in A & y0 <> yo1.x0
proof
consider x,y be set such that
D21: x in A & y in A & x <> y by ZFMISC_1:def 10;
per cases;
suppose C1:yo1.x0 = x;
take y;
thus thesis by C1,D21;
end;
suppose C2:yo1.x0 <> x;
take x;
thus thesis by C2,D21;
end;
end;
then consider y0 be set such that
D2: y0 in A & y0 <> yo1.x0;
defpred C[set] means $1 in Bo2;
deffunc F(set) = yo2.$1;
deffunc G(set) = y0;
D3: for x be set st x in B holds
(C[ x] implies F(x) in A) & (not C[ x] implies G(x) in A)
by D2,FUNCT_2:7;
consider f be Function of B, A such that
D4: for x be set 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(D3);
P1: dom yo2 = Bo2 by FUNCT_2:def 1
.= B /\ Bo2 by XBOOLE_1:28
.= dom f /\ Bo2 by FUNCT_2:def 1;
now let z be set;
assume z in dom yo2;
then z in Bo2;
hence yo2.z = f.z by D4;
end;
then
P2: f|Bo2 = yo2 by P1, FUNCT_1:68;
P3: x0 in dom yo1 by D1,FUNCT_2:def 1;
f.x0 <> yo1.x0 by D2,D4,D1;
then
f|Bo1 <> yo1 by P3, FUNCT_1:68;
hence thesis by P2;
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
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 & f|Bo2 <> yo2 by Lm11;
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 A2;
end;
hence thesis by A2;
end;
suppose Bo2 c= Bo1;
then
consider f be Function of B,A such that
A2: f|Bo2 = yo2 & f|Bo1 <> yo1 by A1,Lm12;
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 A2;
end;
hence thesis by A2;
end;
end;
theorem LM3:
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
AS: Bo1 c= B & Bo2 c= B & cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2);
P1: { y where y is Function of B,A : y|Bo1 = yo1 }
= cylinder0(A,B,Bo1,yo1) by DefX01,AS;
P2: { y where y is Function of B,A : y|Bo2 = yo2 }
= cylinder0(A,B,Bo2,yo2) by DefX01,AS;
hence
Bo1=Bo2 by Lm2,AS,P1;
consider y0 be set such that
P4: y0 in { y where y is Function of B,A : y|Bo1 = yo1 }
by P1,XBOOLE_0:def 1;
consider y be Function of B,A such that
P5: y0=y & y|Bo1 = yo1 by P4;
consider w be Function of B,A such that
P6: y0=w & w|Bo2 = yo2 by P1,P2,AS,P4;
thus yo1=yo2 by Lm2,AS,P1,P2,P5,P6;
end;
theorem LM4:
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
AS: A1 c= A2 & B1 c= B2;
defpred P[set,set] 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);
P1: now let x be set;
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
P2: Bo is finite & D1=cylinder0(A1,B1,Bo,yo1) by Def21;
D13: Bo c= B2 by AS,XBOOLE_1:1;
reconsider yo2=yo1 as Function of Bo,A2 by AS, FUNCT_2:9;
set D2= cylinder0(A2,B2,Bo,yo2);
XXX: D2 is thin_cylinder of A2,B2 by P2,D13,Def21;
reconsider D2 as set;
take D2;
thus D2 in thin_cylinders(A2,B2) & P[x,D2] by P2,XXX;
end;
consider F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2)
such that
P2: for x be set st x in thin_cylinders(A1,B1)
holds P[x,F.x] from FUNCT_2:sch 1(P1);
take F;
thus thesis by P2;
end;
theorem ThMX02:
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[set,set] 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);
P1: now let x be set;
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
P2: Bo2 is finite &
D2=cylinder0(A2,B2,Bo2,yo2) by Def21;
set Bo1=B1 /\ Bo2 /\ (yo2"A1);
XXX: Bo1 c= B1 /\ Bo2 by XBOOLE_1:17;
B1 /\ Bo2 c= B1 by XBOOLE_1:17;then
D13: Bo1 c= B1 by XXX,XBOOLE_1:1;
B1 /\ Bo2 c= Bo2 by XBOOLE_1:17; then
YYY: Bo1 c= Bo2 by XXX,XBOOLE_1:1;
set yo1=yo2 | Bo1;
ZZZ: yo1 is Function of Bo1, A2 by YYY,FUNCT_2:38;
W1:yo2.: (yo2"A1) c= A1 by FUNCT_1:145;
W2: rng yo1 = yo2.: Bo1 by RELAT_1:148;
yo2.: Bo1 c= yo2.: (yo2"A1) by RELAT_1:156,XBOOLE_1:17; then
yo2.: Bo1 c= A1 by XBOOLE_1:1,W1; then
reconsider yo1 as Function of Bo1,A1 by FUNCT_2:8,ZZZ,W2;
set D1= cylinder0(A1,B1,Bo1,yo1);
XXX: D1 is thin_cylinder of A1,B1 by D13,P2,Def21;
reconsider D1 as set;
take D1;
thus D1 in thin_cylinders(A1,B1) & P[x,D1] by P2,XXX,D13;
end;
consider G be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1)
such that
P2: for x be set st x in thin_cylinders(A2,B2)
holds P[x,G.x] from FUNCT_2:sch 1(P1);
take G;
thus thesis by P2;
end;
definition
let A1,A2 be non trivial set, B1,B2 be set;
assume AS: (ex x,y be set st x <> y & x in A1 & y in A1) &
A1 c= 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 LM4,AS;
uniqueness
proof
let F1,F2 be Function of thin_cylinders(A1,B1),
thin_cylinders(A2,B2);
assume
AS1: 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
AS2: 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 set;
assume AS3: x in thin_cylinders(A1,B1);
consider Bo1 being Subset of B1,
yo11 being Function of Bo1,A1,
yo21 being Function of Bo1,A2 such that
P1: Bo1 is finite & yo11=yo21 &
x=cylinder0(A1,B1,Bo1,yo11) &
F1.x=cylinder0(A2,B2,Bo1,yo21) by AS3,AS1;
consider Bo2 being Subset of B1,
yo12 being Function of Bo2,A1,
yo22 being Function of Bo2,A2 such that
P2: Bo2 is finite & yo12=yo22 &
x=cylinder0(A1,B1,Bo2,yo12) &
F2.x=cylinder0(A2,B2,Bo2,yo22) by AS3,AS2;
P3: Bo1 = Bo2 & yo11 = yo12 by LM3,P1,P2;
thus F1.x=F2.x by P1,P2,P3;
end;
hence F1=F2 by FUNCT_2:18;
end;
end;
definition
let A1 be non empty set, A2 be non trivial set, B1,B2 be set;
assume
A1 c= A2 & B1 c= B2;
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 ThMX02;
uniqueness
proof
let F1,F2 be Function of thin_cylinders(A2,B2), thin_cylinders(A1,B1);
assume
AS1: 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
AS2: 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 set;
assume
AS3: x in thin_cylinders(A2,B2);
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
P1: 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) by AS3,AS1;
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
P2: 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) by AS3,AS2;
P3: Bo21 = Bo22 & yo21 = yo22 by LM3,P1,P2;
thus F1.x=F2.x by P1,P2,P3;
end;
hence F1=F2 by FUNCT_2:18;
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
consider Bo be Subset of B, yo be Function of Bo,A such that
A1: Bo is finite &
D = { y where y is Function of B,A : y|Bo = yo } by LM1;
thus thesis by A1;
end;
uniqueness by Lm2;
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
(# Places, Transitions -> non empty set,
S-T_Arcs -> non empty Relation of the Places,the Transitions,
T-S_Arcs -> non empty Relation of the Transitions, the Places,
ColoredSet -> non empty finite set,
firing-rule -> Function #);
end;
definition
let CPNT be Colored_PT_net_Str;
let t0 be transition of CPNT;
attr t0 is outbound means :Def7:
{t0}*' = {};
end;
definition
let CPNT1 be Colored_PT_net_Str;
func Outbds(CPNT1) -> Subset of the Transitions 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 Transitions of CPNT1
proof
let z be set;
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 z in the Transitions of CPNT1;
end;
hence thesis;
end;
end;
definition
let CPNT be Colored_PT_net_Str;
attr CPNT is Colored-PT-net-like means :Def4:
dom (the firing-rule of CPNT)
c= (the Transitions 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_PT_net_Str,
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) by Def4;
theorem LM6:
for CPNT1,CPNT2 be Colored_PT_net_Str,
t1 be transition of CPNT1,t2 be transition of CPNT2 st
the Places of CPNT1 c= the Places of CPNT2
& the Transitions of CPNT1 c= the Transitions 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_PT_net_Str,
t1 be transition of CPNT1,t2 be transition of CPNT2;
assume
AS1: the Places of CPNT1 c= the Places of CPNT2
& the Transitions of CPNT1 c= the Transitions 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;
thus *'{t1} c= *'{t2}
proof
let x be set;
assume x in *'{t1}; then
consider s be place of CPNT1 such that
A1: x=s &
ex f being S-T_arc of CPNT1,
w being transition of CPNT1 st w in {t1} & f = [s,w];
consider f being S-T_arc of CPNT1,
w being transition of CPNT1 such that
A2: w in {t2} & f = [x,w] by AS1,A1;
P1: f is S-T_arc of CPNT2 by AS1,TARSKI:def 3;
x is place of CPNT2 by A1,AS1,TARSKI:def 3;
hence x in *'{t2} by P1,A2;
end;
let x be set;
assume x in {t1}*';
then consider s be place of CPNT1 such that
A1: x=s & ex f being T-S_arc of CPNT1,
w being transition of CPNT1 st w in {t1} & f = [w,s];
consider f being T-S_arc of CPNT1,
w being transition of CPNT1 such that
A2: w in {t2} & f = [w,x] by A1,AS1;
P1: f is T-S_arc of CPNT2 by AS1,TARSKI:def 3;
x is place of CPNT2 by A1,AS1,TARSKI:def 3;
hence x in {t2}*' by P1,A2;
end;
LM7:
for f1,f2,f3,f4,g be Function
st dom f1 /\ dom f2 = {} &
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
AS: dom f1 /\ dom f2 = {} &
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;
set f12 = f1+*f2;
set f123=f1+*f2+*f3;
thus for x be set st x in dom f1 holds g.x=f1.x
proof
let x be set;
assume AS1: x in dom f1;
then
P1: not x in dom f4 by AS,XBOOLE_0:def 4;
P2: not x in dom f3 by AS1,AS,XBOOLE_0:def 4;
P3: not x in dom f2 by AS1,AS,XBOOLE_0:def 4;
thus g.x = f123.x by AS,FUNCT_4:12,P1
.= f12.x by FUNCT_4:12,P2
.= f1.x by FUNCT_4:12,P3;
end;
thus for x be set st x in dom f2 holds g.x=f2.x
proof
let x be set;
assume
AS1: x in dom f2; then
P1: not x in dom f4 by AS,XBOOLE_0:def 4;
P2: not x in dom f3 by AS1,AS,XBOOLE_0:def 4;
thus g.x = f123.x by AS,FUNCT_4:12,P1
.= f12.x by FUNCT_4:12,P2
.= f2.x by FUNCT_4:14,AS1;
end;
thus for x be set st x in dom f3 holds g.x=f3.x
proof
let x be set;
assume AS1: x in dom f3; then
not x in dom f4 by AS,XBOOLE_0:def 4;
hence g.x = f123.x by AS,FUNCT_4:12
.= f3.x by FUNCT_4:14,AS1;
end;
thus for x be set st x in dom f4 holds g.x=f4.x by AS,FUNCT_4:14;
end;
LM8:
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
AS: A /\ B = {} & C c= A & D c= B
& X1 c= A \ C & X2 c= B \ D & X3=C & X4= D;
P1: (A \ C) /\ (B \ D) c= A /\ B by XBOOLE_1:27;
X1 /\ X2 c= (A \ C) /\ (B \ D) by AS,XBOOLE_1:27;
hence X1 /\ X2 = {} by AS,P1;
P2: (A \ C) /\ C = (C /\ A) \ C by XBOOLE_1:49;
C /\ A c= C by XBOOLE_1:17;
then (A \ C) /\ C= {} by XBOOLE_1:37,P2;
hence X1 /\ X3 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
(A \ C) /\ D = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
hence X1 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
(B \ D) /\ C = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
hence X2 /\ X3 = {} by AS,XBOOLE_1:27,XBOOLE_1:3;
P6: (B \ D) /\ D = (B /\ D) \ D by XBOOLE_1:49;
B /\ D c= D by XBOOLE_1:17;
then (B \ D) /\ D= {} by P6,XBOOLE_1:37;
hence X2 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
thus X3 /\ X4 = {} by XBOOLE_1:3,AS,XBOOLE_1:27;
end;
registration
cluster strict Colored-PT-net-like Colored_PT_net_Str;
existence
proof
consider a,b,red,yellow,blue be set;
set PLA={0};
set TRA={a};
set CS = {red,yellow,blue};
set STA = [:PLA,TRA:];
reconsider STA as non empty Relation of PLA,TRA by RELSET_1:def 1;
set TSA= [:TRA,PLA:];
reconsider TSA as non empty Relation of TRA,PLA by RELSET_1:def 1;
consider fa be Function of thin_cylinders(CS,{0}),
thin_cylinders(CS,{0});
set f= ({a} --> fa);
take CPNT = Colored_PT_net_Str
(# PLA,TRA,STA,TSA, CS,f #);
A0: dom f = {a} by FUNCOP_1:19;
now let x be set;
assume
A11: x in dom (the firing-rule of CPNT);
A13: x=a by A0,A11,TARSKI:def 1;
reconsider a1=a as transition of CPNT by TARSKI:def 1;
0 in PLA & a in TRA by TARSKI:def 1;
then [a1,0] in TSA by ZFMISC_1:106;
then
aa: not {a1}*' = {} by PETRI:8;
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 aa,Def7;
end;
hence x in (the Transitions of CPNT) \ Outbds(CPNT) by A13,XBOOLE_0:def 5;
end;
then
A1: dom (the firing-rule of CPNT) c=
(the Transitions of CPNT) \ Outbds(CPNT) by TARSKI:def 3;
now let t be transition of CPNT;
assume t in dom (the firing-rule of CPNT);
P1: t= a by TARSKI:def 1;
P2: 0 in PLA & a in TRA by TARSKI:def 1;
then [a,0] in TSA by ZFMISC_1:106; then
pp: 0 in {t} *' by PETRI:8,P1;
[0,a] in STA by ZFMISC_1:106,P2; then
pa: 0 in *'{t} by PETRI:6,P1;
CS c= CS;
then reconsider CS1= CS as non empty Subset of the ColoredSet of CPNT;
reconsider I = {0} as Subset of *'{t} by pa,ZFMISC_1:37;
reconsider O = {0} as Subset of {t} *' by pp,ZFMISC_1:37;
P7: f.t =fa by FUNCOP_1:13;
fa is Function of thin_cylinders(CS1,I), thin_cylinders(CS1,O );
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 P7;
end;
hence thesis by A1,Def4;
end;
end;
definition
mode Colored-PT-net is Colored-PT-net-like Colored_PT_net_Str;
end;
reserve CPNT for Colored-PT-net;
begin :: Outbound transitions of CPNT
definition
let CPNT1, CPNT2 be Colored_PT_net_Str;
pred CPNT1 misses CPNT2 means :Def7A:
(the Places of CPNT1) /\ (the Places of CPNT2 ) = {} &
(the Transitions of CPNT1) /\ (the Transitions of CPNT2) = {};
symmetry;
end;
begin :: Connecting mapping for CPNT1,CPNT2
definition
let CPNT1 be Colored_PT_net_Str;
let CPNT2 be Colored_PT_net_Str;
mode connecting-mapping of CPNT1,CPNT2 means :Def8:
ex O12 be Function of Outbds(CPNT1), the Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places of CPNT1
st it=[O12,O21];
correctness
proof
consider O12 be Function of Outbds(CPNT1), the Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places 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 means :Def9:
ex q12,q21 be Function,
O12 be Function of Outbds(CPNT1), the Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places 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
consider O12 be Function of Outbds(CPNT1), the Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: O = [O12,O21] by Def8;
set TO1 = Outbds(CPNT1);
set TO2 = Outbds(CPNT2);
set K1=bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT1);
set K2=bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT1);
set L1=bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT2);
set L2=bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT2);
set Y1= PFuncs(K1,K2);
set Y2= PFuncs(L1,L2);
defpred P[set,set] 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) );
P2: for x be set st x in TO1 ex y be set st y in Y1 & P[x,y]
proof
let x be set;
assume x in TO1; then
consider t01 be transition of CPNT1 such that
P21: x=t01 & t01 is outbound;
set t1=*'{t01};
set t2=Im(O12,t01);
consider y be 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);
XH1: H1 c=
bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT1) by LmThin;
XH2: H2 c=
bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT1) by LmThin;
J1: y in Funcs(H1,H2) by FUNCT_2:11;
Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:141; then
J2:y in PFuncs(H1,H2) by J1;
PFuncs(H1,H2) c= PFuncs(K1,K2) by PARTFUN1:128,XH1,XH2;
hence thesis by P21,J2;
end;
consider q12 be Function of TO1,Y1 such that
P3: for x be set st x in TO1 holds P[x,q12.x] from FUNCT_2:sch 1(P2);
P4: 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 P3;
hence q12.tt01 is Function of
thin_cylinders ( the ColoredSet of CPNT1, *'{tt01}),
thin_cylinders ( the ColoredSet of CPNT1, Im(O12,tt01) );
end;
defpred R[set,set] 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));
R2: for x be set st x in TO2 ex y be set st y in Y2 & R[x,y]
proof
let x be set;
assume x in TO2; then
consider t02 be transition of CPNT2 such that
R21: x=t02 & t02 is outbound;
set t1=*'{t02};
set t2= Im(O21,t02);
consider y be 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);
XH1: H1 c=
bool PFuncs(the Places of CPNT2, the ColoredSet of CPNT2) by LmThin;
XH2: H2 c=
bool PFuncs(the Places of CPNT1, the ColoredSet of CPNT2) by LmThin;
J1: y in Funcs(H1,H2) by FUNCT_2:11;
Funcs(H1,H2) c= PFuncs(H1,H2) by FUNCT_2:141;
then
J2:y in PFuncs(H1,H2) by J1;
PFuncs(H1,H2) c= PFuncs(L1,L2) by PARTFUN1:128,XH1,XH2;
hence thesis by R21,J2;
end;
consider q21 be
Function of TO2,Y2 such that
R3: for x be set st x in TO2 holds R[x,q21.x] from FUNCT_2:sch 1(R2);
R4: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 R3;
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];
dom q12=Outbds(CPNT1) & dom q21=Outbds(CPNT2) by FUNCT_2:def 1;
hence thesis by P1,P4,R4;
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
AS: 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 Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places 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 Places of it = (the Places of CPNT1) \/ (the Places of CPNT2) &
the Transitions of it =
(the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
the S-T_Arcs of it =
(the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
the T-S_Arcs of it =
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/ O21 &
the ColoredSet of it = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) &
the firing-rule of it =
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
existence
proof
consider q12,q21 be Function,
O12 be Function of Outbds(CPNT1), the Places of CPNT2,
O21 be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: 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]
by Def9;
reconsider P12 = (the Places of CPNT1) \/ (the Places of CPNT2)
as non empty set;
reconsider T12 = (the Transitions of CPNT1) \/ (the Transitions of CPNT2)
as non empty set;
(the Places of CPNT1) c= P12 & (the Transitions of CPNT1) c= T12
by XBOOLE_1:7; then
reconsider E1=(the S-T_Arcs of CPNT1) as Relation of P12,T12
by RELSET_1:17;
(the Places of CPNT2) c= P12 & (the Transitions of CPNT2) c= T12
by XBOOLE_1:7; then
reconsider E2=(the S-T_Arcs of CPNT2) as Relation of P12,T12
by RELSET_1:17;
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;
(the Transitions of CPNT1) c= T12 & (the Places of CPNT1) c= P12
by XBOOLE_1:7; then
reconsider E21=(the T-S_Arcs of CPNT1) as Relation of T12,P12
by RELSET_1:17;
(the Transitions of CPNT2) c= T12 & (the Places of CPNT2) c= P12
by XBOOLE_1:7; then
reconsider E22=(the T-S_Arcs of CPNT2) as Relation of T12,P12
by RELSET_1:17;
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;
(the Transitions of CPNT1) c= T12 by XBOOLE_1:7; then
L30: Outbds(CPNT1) c= T12 by XBOOLE_1:1;
(the Transitions of CPNT2) c= T12 by XBOOLE_1:7; then
L31: Outbds(CPNT2) c= T12 by XBOOLE_1:1;
L32: the Places of CPNT2 c= P12 by XBOOLE_1:7;
L33: the Places of CPNT1 c= P12 by XBOOLE_1:7;
reconsider E31=O12 as Relation of T12,P12 by L30,L32,RELSET_1:17;
reconsider E32=O21 as Relation of T12,P12 by L31,L33,RELSET_1:17;
reconsider TS12= TTS12 \/ (E31 \/ E32) as non empty Relation of T12,P12;
reconsider CS12 = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) as non empty finite set;
set CR12=
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
set CPNT12=Colored_PT_net_Str (# P12,T12, ST12,TS12,CS12,CR12 #);
set R1=the firing-rule of CPNT1;
set R2=the firing-rule of CPNT2;
set R3=q12;
set R4=q21;
P2: TS12= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/O21
by XBOOLE_1:4;
P22: 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:13; then
x in dom ( R1 +* R2 )
or x in dom R3 or x in dom R4 by FUNCT_4:13;
hence x in dom R1 or x in dom R2
or x in dom R3 or x in dom R4 by FUNCT_4:13;
end;
LM6T1: the Places of CPNT1 c= the Places of CPNT12 by XBOOLE_1:7;
LM6T2: (the Transitions of CPNT1) c= (the Transitions of CPNT12)
by XBOOLE_1:7;
LM6T3: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
Q2: (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) c=
the T-S_Arcs of CPNT12 by XBOOLE_1:7;
(the T-S_Arcs of CPNT1)
c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) by XBOOLE_1:7;
then
LM6T4: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12
by Q2,XBOOLE_1:1;
LM6S1: the Places of CPNT2 c= the Places of CPNT12 by XBOOLE_1:7;
LM6S2: (the Transitions of CPNT2) c= (the Transitions of CPNT12)
by XBOOLE_1:7;
LM6S3: the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
Q2:(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
(the T-S_Arcs of CPNT2)
c= (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
by XBOOLE_1:7;
then
LM6S4: the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12
by Q2,XBOOLE_1:1;
LM7T1: (the Transitions of CPNT1) /\ (the Transitions of CPNT2)
= {} by AS,Def7A;
LM7T4: dom (the firing-rule of CPNT1)
c= (the Transitions of CPNT1) \ (dom q12) by P1,Def4;
LM7T5: dom (the firing-rule of CPNT2)
c= (the Transitions of CPNT2) \ (dom q21) by P1,Def4;
LM7T:
dom (the firing-rule of CPNT1) /\ dom (the firing-rule of CPNT2) = {} &
dom (the firing-rule of CPNT1) /\ dom (the firing-rule of CPNT2) = {} &
dom (the firing-rule of CPNT1) /\ dom q12 = {} &
dom (the firing-rule of CPNT1) /\ dom q21 = {} &
dom (the firing-rule of CPNT2) /\ dom q12 = {} &
dom (the firing-rule of CPNT2) /\ dom q21 = {} &
dom q12 /\ dom q21 ={} by LM8,LM7T1,P1,LM7T4,LM7T5;
s10:now let x be set;
assume x in dom CR12; then
PP1: x in dom R1 or x in dom R2
or x in dom R3 or x in dom R4 by P22;
dom ( the firing-rule of CPNT1)
c= (the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
PP2: dom ( the firing-rule of CPNT1) c= the Transitions of CPNT1
by XBOOLE_1:1;
dom ( the firing-rule of CPNT2)
c= (the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
pp: dom ( the firing-rule of CPNT2) c= the Transitions of CPNT2
by XBOOLE_1:1;
thus x in (the Transitions of CPNT1) \/ (the Transitions of CPNT2)
by XBOOLE_0:def 3,pp,P1,PP1,PP2;
end; then
S10: dom (the firing-rule of CPNT12)
c= the Transitions of CPNT12 by TARSKI:def 3;
SS1: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
SS2: t in dom (the firing-rule of CPNT12);
now per cases by SS2,P22;
suppose
S4: t in dom the firing-rule of CPNT1;
dom ( the firing-rule of CPNT1) c=
(the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
reconsider t1 =t as transition of CPNT1 by S4,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
T6: (the firing-rule of CPNT1).t1
is Function of thin_cylinders(CS1,I1),
thin_cylinders(CS1,O1) by Def4,S4;
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 LM6,LM6T1,LM6T2,LM6T3,LM6T4;
then reconsider I =I1 as Subset of *'{t} by XBOOLE_1:1;
{t1}*' c= {t}*' by LM6,LM6T1,LM6T2,LM6T3,LM6T4;
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 S4,LM7,LM7T,T6;
hence thesis;
end;
suppose
S5: t in dom ( the firing-rule of CPNT2);
dom ( the firing-rule of CPNT2) c=
(the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
reconsider t1 = t as transition of CPNT2 by S5,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
T6: (the firing-rule of CPNT2).t1
is Function of thin_cylinders(CS1,I1),
thin_cylinders(CS1,O1) by Def4,S5;
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 LM6,LM6S1,LM6S2,LM6S3,LM6S4; then
reconsider I =I1 as Subset of *'{t} by XBOOLE_1:1;
{t1}*' c= {t}*' by LM6,LM6S1,LM6S2,LM6S3,LM6S4; 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 S5,LM7,LM7T,T6;
hence thesis;
end;
suppose S6: t in dom (q12);
reconsider t1 =t as transition of CPNT1 by S6,P1;
S610:ex x1 be transition of CPNT1 st t1=x1 & x1 is outbound by S6,P1;
T6: q12.t1 is Function of
thin_cylinders ( the ColoredSet of CPNT1, *'{t1}),
thin_cylinders ( the ColoredSet of CPNT1, Im(O12,t1) ) by P1,S610;
reconsider CS = the ColoredSet of CPNT1
as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
reconsider I =*'{t1} as Subset of *'{t} by LM6,LM6T1,LM6T2,LM6T3,LM6T4;
Im(O12,t1) c= {t}*'
proof
let x be set;
assume
Z: x in Im(O12,t1);
then reconsider s = x as place of CPNT2;
A1: [t1,s] in O12 by Z,RELSET_2:9;
A5: O12 c= E31 \/ E32 by XBOOLE_1:7;
E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7; then
O12 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5; then
reconsider f= [t,s] as T-S_arc of CPNT12 by A1;
A4: s in the Places of CPNT2;
A31:the Places of CPNT2
c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
t in {t} & f=[t,s] by TARSKI:def 1;
hence x in {t}*' by A31,A4;
end;
then reconsider O = Im(O12,t1) as Subset of {t}*';
(the firing-rule of CPNT12).t
is Function of thin_cylinders(CS,I),
thin_cylinders(CS,O) by S6,LM7,LM7T,T6;
hence thesis;
end;
suppose S7: t in dom (q21); then
reconsider t1 = t as transition of CPNT2 by P1;
S610: ex x1 be transition of CPNT2 st t1=x1 & x1 is outbound by S7,P1;
T6: q21.t1 is Function of
thin_cylinders (the ColoredSet of CPNT2, *'{t1}),
thin_cylinders (the ColoredSet of CPNT2, Im(O21,t1) ) by P1,S610;
reconsider CS = the ColoredSet of CPNT2
as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
reconsider
I =*'{t1} as Subset of *'{t} by LM6,LM6S1,LM6S2,LM6S3,LM6S4;
Im(O21,t1) c= {t}*'
proof
let x be set;
assume
Z: x in Im(O21,t1);
then reconsider s=x as place of CPNT1;
A1: [t1,s] in O21 by Z,RELSET_2:9;
A5: O21 c= E31 \/ E32 by XBOOLE_1:7;
E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
then
reconsider f= [t,s] as T-S_arc of CPNT12 by TARSKI:def 3,A1,A5;
A4: s in the Places of CPNT1;
A31: the Places of CPNT1
c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
t in {t} & f=[t,s] by TARSKI:def 1;
hence x in {t}*' by A31,A4;
end;
then reconsider O = Im(O21,t1) as Subset of {t}*';
(the firing-rule of CPNT12).t
is Function of thin_cylinders(CS,I),
thin_cylinders(CS,O) by S7,LM7,LM7T,T6;
hence thesis;
end;
end;
hence thesis;
end;
dom (the firing-rule of CPNT12)
c= (the Transitions of CPNT12) \ Outbds(CPNT12)
proof
let x be set;
assume
ASD: x in dom (the firing-rule of CPNT12); then
reconsider t=x as transition of CPNT12 by s10;
set RR1=the firing-rule of CPNT1;
set RR2=the firing-rule of CPNT2;
set RR3=q12;
set RR4=q21;
now per cases by ASD,P22;
suppose CAS1:t in dom RR1;
Q0: dom ( the firing-rule of CPNT1) c=
(the Transitions of CPNT1) \ Outbds(CPNT1) by Def4; then
Q1: t in the Transitions of CPNT1 & not t in Outbds(CPNT1)
by CAS1,XBOOLE_0:def 5;
reconsider t1 =t as transition of CPNT1 by Q0,CAS1,XBOOLE_0:def 5;
not t1 is outbound by Q1;
then {t1}*' <> {} by Def7;
then
Q2: ex g be set st g in {t1}*' by XBOOLE_0:def 1;
{t1}*' c= {t}*' by LM6,LM6T1,LM6T2,LM6T3,LM6T4; then
not ex w be transition of CPNT12 st t=w & w is outbound by Def7,Q2;
hence not x in Outbds(CPNT12);
end;
suppose CAS2:t in dom RR2;
Q0:dom ( the firing-rule of CPNT2) c=
(the Transitions of CPNT2) \ Outbds(CPNT2) by Def4; then
Q1: t in the Transitions of CPNT2 & not t in Outbds(CPNT2)
by CAS2,XBOOLE_0:def 5;
reconsider t1 =t as transition of CPNT2 by Q0,CAS2,XBOOLE_0:def 5;
not t1 is outbound by Q1;
then {t1}*' <> {} by Def7; then
Q2: ex g be set st g in {t1}*' by XBOOLE_0:def 1;
{t1}*' c= {t}*' by LM6,LM6S1,LM6S2,LM6S3,LM6S4; then
not (ex w be transition of CPNT12 st t=w & w is outbound ) by Def7,Q2;
hence not x in Outbds(CPNT12);
end;
suppose CAS3:t in dom RR3;
t in dom O12 by P1,FUNCT_2:def 1,CAS3; then
consider s be set such that
FF: [t,s] in O12 by RELAT_1:def 4;
reconsider s as place of CPNT2 by FF,ZFMISC_1:106;
A5: O12 c= E31 \/ E32 by XBOOLE_1:7;
E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7; then
O12 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5; then
reconsider f= [t,s] as T-S_arc of CPNT12 by FF;
A4: s in the Places of CPNT2;
A31: the Places of CPNT2
c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
t in {t} & f=[t,s] by TARSKI:def 1; then
s in {t}*' by A4,A31; then
not (ex w be transition of CPNT12 st t=w & w is outbound) by Def7;
hence not x in Outbds(CPNT12);
end;
suppose CAS4:t in dom RR4;
t in dom O21 by P1,FUNCT_2:def 1,CAS4;
then consider s be set such that
FF: [t,s] in O21 by RELAT_1:def 4;
reconsider s as place of CPNT1 by FF,ZFMISC_1:106;
A5: O21 c= E31 \/ E32 by XBOOLE_1:7;
E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
then O21 c= the T-S_Arcs of CPNT12 by XBOOLE_1:1,A5;
then reconsider f= [t,s] as T-S_arc of CPNT12 by FF;
A4: s in the Places of CPNT1;
A31:the Places of CPNT1
c= (the Places of CPNT1) \/ (the Places of CPNT2) by XBOOLE_1:7;
t in {t} & f=[t,s] by TARSKI:def 1;
then s in {t}*' by A31,A4; then
not (ex w be transition of CPNT12 st t=w & w is outbound) by Def7;
hence not x in Outbds(CPNT12);
end;
end;
hence x in (the Transitions of CPNT12) \ Outbds(CPNT12)
by ASD,S10,XBOOLE_0:def 5;
end;
then CPNT12 is Colored-PT-net-like by SS1,Def4;
hence thesis by P1,P2;
end;
uniqueness
proof
let CA,CB be strict Colored-PT-net;
assume
AS1: ex q12A,q21A be Function,
O12A be Function of Outbds(CPNT1), the Places of CPNT2,
O21A be Function of Outbds(CPNT2), the Places 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 Places of CA = (the Places of CPNT1) \/ (the Places of CPNT2) &
the Transitions of CA =
(the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
the S-T_Arcs of CA =
(the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
the T-S_Arcs of CA =
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12A \/ O21A &
the ColoredSet of CA = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) &
the firing-rule of CA =
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12A +* q21A;
assume
BS1: ex q12B,q21B be Function,
O12B be Function of Outbds(CPNT1), the Places of CPNT2,
O21B be Function of Outbds(CPNT2), the Places 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 Places of CB = (the Places of CPNT1) \/ (the Places of CPNT2) &
the Transitions of CB =
(the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
the S-T_Arcs of CB = (the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2)
&
the T-S_Arcs of CB = (the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2)
\/ O12B \/ O21B &
the ColoredSet of CB = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) &
the firing-rule of CB =
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12B +* q21B;
consider q12A,q21A be Function,
O12A be Function of Outbds(CPNT1), the Places of CPNT2,
O21A be Function of Outbds(CPNT2), the Places of CPNT1 such that
P1: 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 Places of CA = (the Places of CPNT1) \/ (the Places of CPNT2) &
the Transitions of CA =
(the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
the S-T_Arcs of CA =
(the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
the T-S_Arcs of CA =
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12A \/O21A &
the ColoredSet of CA = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) &
the firing-rule of CA =
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2)
+* q12A +* q21A by AS1;
consider q12B,q21B be Function,
O12B be Function of Outbds(CPNT1), the Places of CPNT2,
O21B be Function of Outbds(CPNT2), the Places of CPNT1 such that
P2: 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 Places of CB = (the Places of CPNT1) \/ (the Places of CPNT2) &
the Transitions of CB =
(the Transitions of CPNT1) \/ (the Transitions of CPNT2) &
the S-T_Arcs of CB =
(the S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) &
the T-S_Arcs of CB =
(the T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12B \/O21B &
the ColoredSet of CB = (the ColoredSet of CPNT1)
\/ (the ColoredSet of CPNT2) &
the firing-rule of CB =
(the firing-rule of CPNT1) +* (the firing-rule of CPNT2)
+* q12B +* q21B by BS1;
P3: q12A=q12B & q21A =q21B by P1,P2,ZFMISC_1:33;
O12A=O12B & O21A =O21B by P1,P2,ZFMISC_1:33;
hence thesis by P1,P2,P3;
end;
end;