:: Formulation of Cell Petri Nets
:: by Mitsuru Jitsukawa , Pauline N. Kawamoto and Yasunari Shidama
::
:: Copyright (c) 2013-2021 Association of Mizar Users

definition
let I be non empty set ;
let CPNTS be ManySortedSet of I;
attr CPNTS is Colored-PT-net-Family-like means :Def11a: :: PETRI_3:def 1
for i being Element of I holds CPNTS . i is Colored-PT-net;
end;

:: deftheorem Def11a defines Colored-PT-net-Family-like PETRI_3:def 1 :
for I being non empty set
for CPNTS being ManySortedSet of I holds
( CPNTS is Colored-PT-net-Family-like iff for i being Element of I holds CPNTS . i is Colored-PT-net );

registration
let I be non empty set ;
existence
ex b1 being ManySortedSet of I st b1 is Colored-PT-net-Family-like
proof end;
end;

definition end;

definition
let I be non empty set ;
let CPNTS be Colored-PT-net-Family of I;
let i be Element of I;
:: original: .
redefine func CPNTS . i -> Colored-PT-net;
correctness
coherence
CPNTS . i is Colored-PT-net
;
by Def11a;
end;

definition
let I be non empty set ;
let CPNT be Colored-PT-net-Family of I;
attr CPNT is disjoint_valued means :: PETRI_3:def 2
for i, j being Element of I st i <> j holds
( the carrier of (CPNT . i) misses the carrier of (CPNT . j) & the carrier' of (CPNT . i) misses the carrier' of (CPNT . j) );
end;

:: deftheorem defines disjoint_valued PETRI_3:def 2 :
for I being non empty set
for CPNT being Colored-PT-net-Family of I holds
( CPNT is disjoint_valued iff for i, j being Element of I st i <> j holds
( the carrier of (CPNT . i) misses the carrier of (CPNT . j) & the carrier' of (CPNT . i) misses the carrier' of (CPNT . j) ) );

theorem LM01: :: PETRI_3:1
for I being set
for F, D, R being ManySortedSet of I st ( for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . 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 ) holds
ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
proof end;

theorem LM03: :: PETRI_3:2
for I being set
for Y, Z being ManySortedSet of I st ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union (Y (\) Z) = () \ ()
proof end;

theorem LM04: :: PETRI_3:3
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y (\) Z & ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union X c= () \ ()
proof end;

LMXorDelta: for I being non trivial set ex i, j being Element of I st i <> j
proof end;

definition
let I be non trivial set ;
func XorDelta I -> non empty set equals :: PETRI_3:def 3
{ [i,j] where i, j is Element of I : i <> j } ;
correctness
coherence
{ [i,j] where i, j is Element of I : i <> j } is non empty set
;
proof end;
end;

:: deftheorem defines XorDelta PETRI_3:def 3 :
for I being non trivial set holds XorDelta I = { [i,j] where i, j is Element of I : i <> j } ;

theorem SYLM2: :: PETRI_3:4
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I holds not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty
proof end;

definition
let I be non trivial finite set ;
let CPNT be Colored-PT-net-Family of I;
mode connecting-mapping of CPNT -> ManySortedSet of XorDelta I means :Defcntmap: :: PETRI_3:def 4
( rng it c= union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } & ( for i, j being Element of I st i <> j holds
it . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) );
existence
ex b1 being ManySortedSet of XorDelta I st
( rng b1 c= union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } & ( for i, j being Element of I st i <> j holds
b1 . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) )
proof end;
end;

:: deftheorem Defcntmap defines connecting-mapping PETRI_3:def 4 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for b3 being ManySortedSet of XorDelta I holds
( b3 is connecting-mapping of CPNT iff ( rng b3 c= union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } & ( for i, j being Element of I st i <> j holds
b3 . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) ) );

theorem SYLM3: :: PETRI_3:5
for CPNT1, CPNT2 being Colored-PT-net
for O12 being Function of (Outbds CPNT1), the carrier of CPNT2
for q12 being Function st dom q12 = Outbds CPNT1 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) holds
q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ))
proof end;

definition
let I be non trivial finite set ;
let CPNT be Colored-PT-net-Family of I;
let O be connecting-mapping of CPNT;
mode connecting-firing-rule of O -> ManySortedSet of XorDelta I means :Defcntfir: :: PETRI_3:def 5
for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = it . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) );
existence
ex b1 being ManySortedSet of XorDelta I st
for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = b1 . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) )
proof end;
end;

:: deftheorem Defcntfir defines connecting-firing-rule PETRI_3:def 5 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for O being connecting-mapping of CPNT
for b4 being ManySortedSet of XorDelta I holds
( b4 is connecting-firing-rule of O iff for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = b4 . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) );

LMQ1: for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I st CPNT is disjoint_valued holds
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )

proof end;

LMQ1A: for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O
for F being Function st F = union (rng q) holds
for g being Function
for x being object
for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds
F . x = g . x

proof end;

definition
let I be non trivial finite set ;
let CPNT be Colored-PT-net-Family of I;
let O be connecting-mapping of CPNT;
let q be connecting-firing-rule of O;
assume AS: ( CPNT is disjoint_valued & ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) ) ;
func synthesis q -> strict Colored-PT-net means :: PETRI_3:def 6
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 it = union (rng P) & the carrier' of it = union (rng T) & the S-T_Arcs of it = union (rng ST) & the T-S_Arcs of it = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of it = union (rng CS) & the firing-rule of it = UF +* UQ );
existence
ex b1 being strict Colored-PT-net 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 b1 = union (rng P) & the carrier' of b1 = union (rng T) & the S-T_Arcs of b1 = union (rng ST) & the T-S_Arcs of b1 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b1 = union (rng CS) & the firing-rule of b1 = UF +* UQ )
proof end;
uniqueness
for b1, b2 being strict Colored-PT-net st 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 b1 = union (rng P) & the carrier' of b1 = union (rng T) & the S-T_Arcs of b1 = union (rng ST) & the T-S_Arcs of b1 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b1 = union (rng CS) & the firing-rule of b1 = UF +* UQ ) & 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 b2 = union (rng P) & the carrier' of b2 = union (rng T) & the S-T_Arcs of b2 = union (rng ST) & the T-S_Arcs of b2 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b2 = union (rng CS) & the firing-rule of b2 = UF +* UQ ) holds
b1 = b2
proof end;
end;

:: deftheorem defines synthesis PETRI_3:def 6 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st CPNT is disjoint_valued & ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
for b5 being strict Colored-PT-net holds
( b5 = synthesis q iff 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 b5 = union (rng P) & the carrier' of b5 = union (rng T) & the S-T_Arcs of b5 = union (rng ST) & the T-S_Arcs of b5 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b5 = union (rng CS) & the firing-rule of b5 = UF +* UQ ) );

definition
let I be non empty finite set ;
let CPNT be Colored-PT-net-Family of I;
attr CPNT is Cell-Petri-nets means :: PETRI_3:def 7
ex N being Function of I,(bool (rng CPNT)) st
for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : j <> i } ;
end;

:: deftheorem defines Cell-Petri-nets PETRI_3:def 7 :
for I being non empty finite set
for CPNT being Colored-PT-net-Family of I holds
( CPNT is Cell-Petri-nets iff ex N being Function of I,(bool (rng CPNT)) st
for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : j <> i } );

definition
let I be non trivial finite set ;
let CPNT be Colored-PT-net-Family of I;
let N be Function of I,(bool (rng CPNT));
let O be connecting-mapping of CPNT;
pred N,O is_Cell-Petri-nets means :: PETRI_3:def 8
for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : ( j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) } ;
end;

:: deftheorem defines is_Cell-Petri-nets PETRI_3:def 8 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT holds
( N,O is_Cell-Petri-nets iff for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : ( j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) } );

theorem :: PETRI_3:6
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i
proof end;

:: non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;
definition
let CPN be Colored_PT_net_Str ;
:: non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;
attr CPN is with-nontrivial-ColoredSet means :defnontrivial: :: PETRI_3:def 9
not the ColoredSet of CPN is trivial ;
end;

:: deftheorem defnontrivial defines with-nontrivial-ColoredSet PETRI_3:def 9 :
for CPN being Colored_PT_net_Str holds
( CPN is with-nontrivial-ColoredSet iff not the ColoredSet of CPN is trivial );

registration
existence
proof end;
end;

registration
let CPNT be with-nontrivial-ColoredSet Colored-PT-net;
cluster the ColoredSet of CPNT -> non trivial ;
correctness
coherence
not the ColoredSet of CPNT is trivial
;
by defnontrivial;
end;

::Def13:: color-threshold
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let S be Subset of the carrier of CPN;
let D be thin_cylinder of the ColoredSet of CPN,S;
mode color-threshold of D is Function of (loc D), the ColoredSet of CPN;
end;

:: color-count of CPN
definition
let CPN be Colored-PT-net;
mode color-count of CPN is Function of the ColoredSet of CPN,NAT;
end;

:: Colored-states of CPN
definition
let CPN be Colored-PT-net;
func Colored-states CPN -> non empty set equals :: PETRI_3:def 10
{ e where e is color-count of CPN : verum } ;
coherence
{ e where e is color-count of CPN : verum } is non empty set
proof end;
end;

:: deftheorem defines Colored-states PETRI_3:def 10 :
for CPN being Colored-PT-net holds Colored-states CPN = { e where e is color-count of CPN : verum } ;

:: colored-state of CPN
definition
let CPN be Colored-PT-net;
mode colored-state of CPN is Function of CPN,();
end;

definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let p be place of CPN;
:: original: .
redefine func m . p -> color-count of CPN;
correctness
coherence
m . p is color-count of CPN
;
proof end;
end;

definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let mp be color-count of CPN;
let x be object ;
:: original: .
redefine func mp . x -> Element of NAT ;
correctness
coherence
mp . x is Element of NAT
;
proof end;
end;

:: q-firable on m
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
let D be thin_cylinder of the ColoredSet of CPN, *' {t};
let ColD be color-threshold of D;
:: :Def14:
pred t is_firable_on m,ColD means :: PETRI_3:def 11
( the firing-rule of CPN . [t,D] <> {} & ( for p being place of CPN st p in loc D holds
1 <= (m . p) . (ColD . p) ) );
end;

:: deftheorem defines is_firable_on PETRI_3:def 11 :
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN, *' {t}
for ColD being color-threshold of D holds
( t is_firable_on m,ColD iff ( the firing-rule of CPN . [t,D] <> {} & ( for p being place of CPN st p in loc D holds
1 <= (m . p) . (ColD . p) ) ) );

:: q-firable set on t
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
:: :Def15:
func firable_set_on (m,t) -> set equals :: PETRI_3:def 12
{ D where D is thin_cylinder of the ColoredSet of CPN, *' {t} : ex ColD being color-threshold of D st t is_firable_on m,ColD } ;
coherence
{ D where D is thin_cylinder of the ColoredSet of CPN, *' {t} : ex ColD being color-threshold of D st t is_firable_on m,ColD } is set
;
end;

:: deftheorem defines firable_set_on PETRI_3:def 12 :
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN holds firable_set_on (m,t) = { D where D is thin_cylinder of the ColoredSet of CPN, *' {t} : ex ColD being color-threshold of D st t is_firable_on m,ColD } ;

:: t is q-firable on m iff q-firable set on t, m
theorem :: PETRI_3:7
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN, *' {t} holds
( ex ColD being color-threshold of D st t is_firable_on m,ColD iff D in firable_set_on (m,t) )
proof end;

:: The definition of mapping Ptr_Sub
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
let D be thin_cylinder of the ColoredSet of CPN, *' {t};
let ColD be color-threshold of D;
let p be Element of CPN;
assume AS1: t is_firable_on m,ColD ;
func Ptr_Sub (ColD,m,p) -> Function of the ColoredSet of CPN,NAT means :Def16Sub: :: PETRI_3:def 13
for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies it . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies it . x = (m . p) . x ) );
existence
ex b1 being Function of the ColoredSet of CPN,NAT st
for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b1 . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b1 . x = (m . p) . x ) )
proof end;
uniqueness
for b1, b2 being Function of the ColoredSet of CPN,NAT st ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b1 . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b1 . x = (m . p) . x ) ) ) & ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b2 . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b2 . x = (m . p) . x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16Sub defines Ptr_Sub PETRI_3:def 13 :
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN, *' {t}
for ColD being color-threshold of D
for p being Element of CPN st t is_firable_on m,ColD holds
for b7 being Function of the ColoredSet of CPN,NAT holds
( b7 = Ptr_Sub (ColD,m,p) iff for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b7 . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b7 . x = (m . p) . x ) ) );

:: The definition of mapping Ptr_Add
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
let D be thin_cylinder of the ColoredSet of CPN,{t} *' ;
let ColD be color-threshold of D;
let p be Element of CPN;
func Ptr_Add (ColD,m,p) -> Function of the ColoredSet of CPN,NAT means :Def16Add: :: PETRI_3:def 14
for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies it . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies it . x = (m . p) . x ) );
existence
ex b1 being Function of the ColoredSet of CPN,NAT st
for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b1 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b1 . x = (m . p) . x ) )
proof end;
uniqueness
for b1, b2 being Function of the ColoredSet of CPN,NAT st ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b1 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b1 . x = (m . p) . x ) ) ) & ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b2 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b2 . x = (m . p) . x ) ) ) holds
b1 = b2
proof end;
end;

for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD being color-threshold of D
for p being Element of CPN
for b7 being Function of the ColoredSet of CPN,NAT holds
( b7 = Ptr_Add (ColD,m,p) iff for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b7 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b7 . x = (m . p) . x ) ) );

:: The definition of firing_result
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
let D be thin_cylinder of the ColoredSet of CPN, *' {t};
let E be thin_cylinder of the ColoredSet of CPN,{t} *' ;
let ColD be color-threshold of D;
let ColE be color-threshold of E;
let p be Element of CPN;
func firing_result (ColD,ColE,m,p) -> Function of the ColoredSet of CPN,NAT equals :Def16: :: PETRI_3:def 15
Ptr_Sub (ColD,m,p) if ( t is_firable_on m,ColD & p in (loc D) \ (loc E) )
Ptr_Add (ColE,m,p) if ( t is_firable_on m,ColD & p in (loc E) \ (loc D) )
otherwise m . p;
coherence
( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies Ptr_Sub (ColD,m,p) is Function of the ColoredSet of CPN,NAT ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies Ptr_Add (ColE,m,p) is Function of the ColoredSet of CPN,NAT ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies m . p is Function of the ColoredSet of CPN,NAT ) )
;
consistency
for b1 being Function of the ColoredSet of CPN,NAT st t is_firable_on m,ColD & p in (loc D) \ (loc E) & t is_firable_on m,ColD & p in (loc E) \ (loc D) holds
( b1 = Ptr_Sub (ColD,m,p) iff b1 = Ptr_Add (ColE,m,p) )
proof end;
end;

:: deftheorem Def16 defines firing_result PETRI_3:def 15 :
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D being thin_cylinder of the ColoredSet of CPN, *' {t}
for E being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD being color-threshold of D
for ColE being color-threshold of E
for p being Element of CPN holds
( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies firing_result (ColD,ColE,m,p) = Ptr_Sub (ColD,m,p) ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies firing_result (ColD,ColE,m,p) = Ptr_Add (ColE,m,p) ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies firing_result (ColD,ColE,m,p) = m . p ) );

:: The definition of the range of firing_result
theorem :: PETRI_3:8
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D0 being thin_cylinder of the ColoredSet of CPN, *' {t}
for D1 being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD0 being color-threshold of D0
for ColD1 being color-threshold of D1
for x being Element of the ColoredSet of CPN
for p being Element of CPN holds
( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
proof end;

theorem :: PETRI_3:9
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D0 being thin_cylinder of the ColoredSet of CPN, *' {t}
for D1 being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD0 being color-threshold of D0
for ColD1 being color-threshold of D1
for x being Element of the ColoredSet of CPN
for p being Element of CPN st t is outbound holds
( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x )
proof end;