deffunc H1( Element of I) -> set = the carrier of (CPNT . $1);
consider P being ManySortedSet of I such that
AS1:
for i being Element of I holds P . i = H1(i)
from PBOOLE:sch 5();
deffunc H2( Element of I) -> set = the carrier' of (CPNT . $1);
consider T being ManySortedSet of I such that
AS2:
for i being Element of I holds T . i = H2(i)
from PBOOLE:sch 5();
deffunc H3( Element of I) -> Element of bool [: the carrier of (CPNT . $1), the carrier' of (CPNT . $1):] = the S-T_Arcs of (CPNT . $1);
consider ST being ManySortedSet of I such that
AS3:
for i being Element of I holds ST . i = H3(i)
from PBOOLE:sch 5();
deffunc H4( Element of I) -> Element of bool [: the carrier' of (CPNT . $1), the carrier of (CPNT . $1):] = the T-S_Arcs of (CPNT . $1);
consider TS being ManySortedSet of I such that
AS4:
for i being Element of I holds TS . i = H4(i)
from PBOOLE:sch 5();
deffunc H5( Element of I) -> set = the ColoredSet of (CPNT . $1);
consider CS being ManySortedSet of I such that
AS5:
for i being Element of I holds CS . i = H5(i)
from PBOOLE:sch 5();
deffunc H6( Element of I) -> set = the firing-rule of (CPNT . $1);
consider F being ManySortedSet of I such that
AS6:
for i being Element of I holds F . i = H6(i)
from PBOOLE:sch 5();
deffunc H7( Element of I) -> set = dom the firing-rule of (CPNT . $1);
consider DM being ManySortedSet of I such that
DM1:
for i being Element of I holds DM . i = H7(i)
from PBOOLE:sch 5();
deffunc H8( Element of I) -> set = rng the firing-rule of (CPNT . $1);
consider RG being ManySortedSet of I such that
RG1:
for i being Element of I holds RG . i = H8(i)
from PBOOLE:sch 5();
set i = the Element of I;
P . the Element of I = the carrier of (CPNT . the Element of I)
by AS1;
then consider x being object such that
S1:
x in P . the Element of I
by XBOOLE_0:def 1;
reconsider P0 = union (rng P) as non empty set by S1, TARSKI:def 4;
set i = the Element of I;
T . the Element of I = the carrier' of (CPNT . the Element of I)
by AS2;
then consider x being object such that
S2:
x in T . the Element of I
by XBOOLE_0:def 1;
reconsider T0 = union (rng T) as non empty set by S2, TARSKI:def 4;
s:
for X being set st X in rng ST holds
X c= [:P0,T0:]
set i = the Element of I;
ST . the Element of I = the S-T_Arcs of (CPNT . the Element of I)
by AS3;
then consider x being object such that
S1:
x in ST . the Element of I
by XBOOLE_0:def 1;
reconsider ST0 = union (rng ST) as non empty Relation of P0,T0 by S1, TARSKI:def 4, s, ZFMISC_1:76;
for X being set st X in rng TS holds
X c= [:T0,P0:]
then PTS0:
union (rng TS) c= [:T0,P0:]
by ZFMISC_1:76;
for X being set st X in rng O holds
X c= [:T0,P0:]
proof
let X be
set ;
( X in rng O implies X c= [:T0,P0:] )
assume
X in rng O
;
X c= [:T0,P0:]
then consider z being
object such that L1:
(
z in dom O &
X = O . z )
by FUNCT_1:def 3;
z in XorDelta I
by L1;
then consider i,
j being
Element of
I such that L11:
(
z = [i,j] &
i <> j )
;
l12:
O . [i,j] is
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j)
by L11, Defcntmap;
L14:
( the
carrier' of
(CPNT . i) = T . i & the
carrier of
(CPNT . j) = P . j )
by AS1, AS2;
L4:
T . i c= T0
by ZFMISC_1:74;
P . j c= P0
by ZFMISC_1:74;
then L13:
[:(T . i),(P . j):] c= [:T0,P0:]
by L4, ZFMISC_1:96;
[:(Outbds (CPNT . i)), the carrier of (CPNT . j):] c= [:(T . i),(P . j):]
by L14, ZFMISC_1:96;
hence
X c= [:T0,P0:]
by L13, l12, L11, L1;
verum
end;
then t:
union (rng O) c= [:T0,P0:]
by ZFMISC_1:76;
set i = the Element of I;
TS . the Element of I = the T-S_Arcs of (CPNT . the Element of I)
by AS4;
then consider x being object such that
S1:
x in TS . the Element of I
by XBOOLE_0:def 1;
x in union (rng TS)
by S1, TARSKI:def 4;
then reconsider TS0 = (union (rng TS)) \/ (union (rng O)) as non empty Relation of T0,P0 by t, PTS0, XBOOLE_1:8;
LL0:
for X being set st X in rng CS holds
X is finite
ll3:
dom CS is finite
;
set i = the Element of I;
CS . the Element of I = the ColoredSet of (CPNT . the Element of I)
by AS5;
then consider x being object such that
S5:
x in CS . the Element of I
by XBOOLE_0:def 1;
reconsider CS0 = union (rng CS) as non empty finite set by S5, TARSKI:def 4, LL0, ll3, FINSET_1:7, FINSET_1:8;
LL41:
for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = DM . i & rng f = RG . i )
for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g
then consider F0 being Function such that
LL43:
( F0 = union (rng F) & dom F0 = union (rng DM) & rng F0 = union (rng RG) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
F0 . x = f . x ) )
by LM01, LL41;
reconsider UQ = union (rng q) as Function by LMQ1, AS;
set UF0 = F0 +* UQ;
reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored_Petri_net by PETRI:def 1, PETRI:def 2;
deffunc H9( Element of I) -> Element of bool the carrier' of (CPNT . $1) = Outbds (CPNT . $1);
consider OU being Function such that
OU1:
( dom OU = I & ( for i being Element of I holds OU . i = H9(i) ) )
from FUNCT_1:sch 4();
reconsider OU = OU as I -defined Function by OU1, RELAT_1:def 18;
reconsider OU = OU as ManySortedSet of I by OU1, PARTFUN1:def 2;
for x0 being object st x0 in Outbds SCPNT holds
x0 in union (rng OU)
then OU2:
Outbds SCPNT c= union (rng OU)
;
XX3:
for i, j being object st i in I & j in I & i <> j holds
(T . i) /\ (OU . j) = {}
v:
for i being object st i in I holds
DM . i c= (T (\) OU) . i
XXX2:
( union (rng DM) = Union DM & union (rng T) = Union T & union (rng OU) = Union OU )
by CARD_3:def 4;
then XXX3A:
dom F0 c= the carrier' of SCPNT \ (Union OU)
by LL43, v, LM04, XX3, PBOOLE:def 2;
xx:
the carrier' of SCPNT \ (union (rng OU)) c= the carrier' of SCPNT \ (Outbds SCPNT)
by OU2, XBOOLE_1:34;
for x being object st x in dom the firing-rule of SCPNT holds
x in the carrier' of SCPNT \ (Outbds SCPNT)
proof
let x be
object ;
( x in dom the firing-rule of SCPNT implies x in the carrier' of SCPNT \ (Outbds SCPNT) )
assume
x in dom the
firing-rule of
SCPNT
;
x in the carrier' of SCPNT \ (Outbds SCPNT)
per cases then
( x in dom F0 or x in dom UQ )
by FUNCT_4:12;
suppose AG1:
x in dom UQ
;
x in the carrier' of SCPNT \ (Outbds SCPNT)consider s being
object such that D2:
[x,s] in UQ
by AG1, XTUPLE_0:def 12;
consider i,
j being
Element of
I,
q12 being
Function,
O12 being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) such that D3:
(
i <> j & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
q12 . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) &
q12 in Funcs (
(Outbds (CPNT . i)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) &
q12 = q . [i,j] &
O12 = O . [i,j] &
[x,s] in q12 )
by LMQ1, AS, D2;
CT1:
( the
carrier' of
(CPNT . i) = T . i & the
carrier of
(CPNT . j) = P . j )
by AS1, AS2;
x in dom q12
by D3, XTUPLE_0:def 12;
then S0:
x in Outbds (CPNT . i)
by D3, FUNCT_2:92;
w:
T . i c= T0
by ZFMISC_1:74;
then S2:
x in the
carrier' of
SCPNT
by S0, CT1;
reconsider t =
x as
transition of
SCPNT by w, S0, CT1;
t in dom O12
by S0, FUNCT_2:def 1;
then consider s being
object such that A65:
[t,s] in O12
by XTUPLE_0:def 12;
[i,j] in XorDelta I
by D3;
then
[i,j] in dom O
by PARTFUN1:def 2;
then
O . [i,j] in rng O
by FUNCT_1:3;
then
[t,s] in union (rng O)
by D3, A65, TARSKI:def 4;
then reconsider f =
[t,s] as
T-S_arc of
SCPNT by XBOOLE_0:def 3;
A68:
f = [t,s]
;
A69:
t in {t}
by TARSKI:def 1;
U2:
s in the
carrier of
(CPNT . j)
by A65, ZFMISC_1:87;
P . j c= P0
by ZFMISC_1:74;
then
s in {t} *'
by A69, A68, U2, CT1;
then
for
w being
transition of
SCPNT holds
( not
t = w or not
w is
outbound )
;
then
not
x in Outbds SCPNT
;
hence
x in the
carrier' of
SCPNT \ (Outbds SCPNT)
by S2, XBOOLE_0:def 5;
verum end;
end;
then CP1:
dom the firing-rule of SCPNT c= the carrier' of SCPNT \ (Outbds SCPNT)
;
for t being transition of SCPNT st t in dom the firing-rule of SCPNT holds
ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
proof
let t be
transition of
SCPNT;
( t in dom the firing-rule of SCPNT implies ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) )
assume d:
t in dom the
firing-rule of
SCPNT
;
ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
per cases
( not t in dom UQ or t in dom UQ )
;
suppose AG01:
not
t in dom UQ
;
ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))then AG0:
t in dom F0
by d, FUNCT_4:12;
consider Z being
set such that XOU3:
(
t in Z &
Z in rng T )
by TARSKI:def 4;
consider i being
object such that XOU4:
(
i in dom T &
Z = T . i )
by XOU3, FUNCT_1:def 3;
reconsider i =
i as
Element of
I by XOU4;
reconsider ti =
t as
transitions of
(CPNT . i) by XOU3, XOU4, AS2;
consider Z being
set such that POU3:
(
t in Z &
Z in rng DM )
by LL43, AG0, TARSKI:def 4;
consider j being
object such that POU4:
(
j in dom DM &
Z = DM . j )
by POU3, FUNCT_1:def 3;
reconsider j =
j as
Element of
I by POU4;
OU6:
DM . j = dom the
firing-rule of
(CPNT . j)
by DM1;
i = j
then OU8:
ti in dom the
firing-rule of
(CPNT . i)
by POU3, POU4, DM1;
consider CSi being non
empty Subset of the
ColoredSet of
(CPNT . i),
Ii being
Subset of
(*' {ti}),
Oi being
Subset of
({ti} *') such that OU9:
the
firing-rule of
(CPNT . i) . ti is
Function of
(thin_cylinders (CSi,Ii)),
(thin_cylinders (CSi,Oi))
by PETRI_2:def 11, OU8;
CC1:
CS . i c= union (rng CS)
by ZFMISC_1:74;
CS . i = the
ColoredSet of
(CPNT . i)
by AS5;
then reconsider CS =
CSi as non
empty Subset of the
ColoredSet of
SCPNT by CC1, XBOOLE_1:1;
Ii c= *' {t}
then reconsider I0 =
Ii as
Subset of
(*' {t}) ;
Oi c= {t} *'
then reconsider O =
Oi as
Subset of
({t} *') ;
Y1:
F . i = the
firing-rule of
(CPNT . i)
by AS6;
the
firing-rule of
SCPNT . t =
F0 . t
by AG01, FUNCT_4:11
.=
the
firing-rule of
(CPNT . i) . ti
by Y1, OU8, LL43
;
then
the
firing-rule of
SCPNT . t is
Function of
(thin_cylinders (CS,I0)),
(thin_cylinders (CS,O))
by OU9;
hence
ex
CS being non
empty Subset of the
ColoredSet of
SCPNT ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *') st the
firing-rule of
SCPNT . t is
Function of
(thin_cylinders (CS,I)),
(thin_cylinders (CS,O))
;
verum end; suppose AG1:
t in dom UQ
;
ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))then consider s being
object such that D2:
[t,s] in UQ
by XTUPLE_0:def 12;
consider i,
j being
Element of
I,
q12 being
Function,
O12 being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) such that D3:
(
i <> j & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
q12 . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) &
q12 in Funcs (
(Outbds (CPNT . i)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) &
q12 = q . [i,j] &
O12 = O . [i,j] &
[t,s] in q12 )
by LMQ1, AS, D2;
CT1:
the
ColoredSet of
(CPNT . i) = CS . i
by AS5;
DF1:
t in dom q12
by D3, XTUPLE_0:def 12;
then S0:
t in Outbds (CPNT . i)
by D3, FUNCT_2:92;
then reconsider ti =
t as
transition of
(CPNT . i) ;
v8:
ex
x being
transition of
(CPNT . i) st
(
ti = x &
x is
outbound )
by S0;
CS . i = the
ColoredSet of
(CPNT . i)
by AS5;
then reconsider CS0 =
CS . i as non
empty Subset of the
ColoredSet of
SCPNT by ZFMISC_1:74;
*' {ti} c= *' {t}
then reconsider I0 =
*' {ti} as
Subset of
(*' {t}) ;
Im (
O12,
ti)
c= {t} *'
proof
let x be
object ;
TARSKI:def 3 ( not x in Im (O12,ti) or x in {t} *' )
assume A41:
x in Im (
O12,
ti)
;
x in {t} *'
then reconsider sj =
x as
place of
(CPNT . j) ;
A42:
[ti,sj] in O12
by A41, RELSET_2:9;
[i,j] in XorDelta I
by D3;
then
[i,j] in dom O
by PARTFUN1:def 2;
then
O . [i,j] in rng O
by FUNCT_1:3;
then
[ti,sj] in union (rng O)
by D3, A42, TARSKI:def 4;
then reconsider f =
[t,sj] as
T-S_arc of
SCPNT by XBOOLE_0:def 3;
CT1:
the
carrier of
(CPNT . j) = P . j
by AS1;
P . j c= P0
by ZFMISC_1:74;
then reconsider s =
sj as
place of
SCPNT by CT1;
A44:
f = [t,s]
;
t in {t}
by TARSKI:def 1;
hence
x in {t} *'
by A44;
verum
end; then reconsider O0 =
Im (
O12,
ti) as
Subset of
({t} *') ;
the
firing-rule of
SCPNT . t =
UQ . t
by AG1, FUNCT_4:13
.=
q12 . ti
by DF1, D3, LMQ1A
;
then
the
firing-rule of
SCPNT . t is
Function of
(thin_cylinders (CS0,I0)),
(thin_cylinders (CS0,O0))
by v8, CT1, D3;
hence
ex
CS being non
empty Subset of the
ColoredSet of
SCPNT ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *') st the
firing-rule of
SCPNT . t is
Function of
(thin_cylinders (CS,I)),
(thin_cylinders (CS,O))
;
verum end;
end;
then reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored-PT-net by PETRI_2:def 11, CP1;
take
SCPNT
; ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ )
thus
ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ )
by AS1, AS2, AS3, AS4, AS5, AS6, LL43; verum