let CPN be with-nontrivial-ColoredSet Colored-PT-net; :: thesis: 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 )

let m be colored-state of CPN; :: thesis: 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 )

let t be Element of the carrier' of CPN; :: thesis: 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 )

let D0 be thin_cylinder of the ColoredSet of CPN, *' {t}; :: thesis: 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 )

let D1 be thin_cylinder of the ColoredSet of CPN,{t} *' ; :: thesis: 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 )

let ColD0 be color-threshold of D0; :: thesis: 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 )

let ColD1 be color-threshold of D1; :: thesis: 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 )

let x be Element of the ColoredSet of CPN; :: thesis: 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 )

let p be Element of CPN; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
per cases ( ( p in (loc D0) \ (loc D1) & t is_firable_on m,ColD0 ) or ( p in (loc D1) \ (loc D0) & t is_firable_on m,ColD0 ) or ( ( not p in (loc D0) \ (loc D1) or not t is_firable_on m,ColD0 ) & ( not p in (loc D1) \ (loc D0) or not t is_firable_on m,ColD0 ) ) ) ;
suppose A1: ( p in (loc D0) \ (loc D1) & t is_firable_on m,ColD0 ) ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A11: firing_result (ColD0,ColD1,m,p) = Ptr_Sub (ColD0,m,p) by Def16;
A12: p in loc D0 by ;
per cases ( x = ColD0 . p or x <> ColD0 . p ) ;
suppose a: x = ColD0 . p ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
(((m . p) . x) - 1) + 0 <= (((m . p) . x) - 1) + 2 by XREAL_1:7;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 ) by ; :: thesis: verum
end;
suppose a: x <> ColD0 . p ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A122: (firing_result (ColD0,ColD1,m,p)) . x = (m . p) . x by ;
A123: ((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by ;
((m . p) . x) + 0 <= ((m . p) . x) + 1 by XREAL_1:7;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 ) by ; :: thesis: verum
end;
end;
end;
suppose A2: ( p in (loc D1) \ (loc D0) & t is_firable_on m,ColD0 ) ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A11: firing_result (ColD0,ColD1,m,p) = Ptr_Add (ColD1,m,p) by Def16;
A12: p in loc D1 by ;
per cases ( x = ColD1 . p or x <> ColD1 . p ) ;
suppose x = ColD1 . p ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A122: (firing_result (ColD0,ColD1,m,p)) . x = ((m . p) . x) + 1 by ;
(((m . p) . x) - 1) + 0 <= (((m . p) . x) - 1) + 2 by XREAL_1:7;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 ) by A122; :: thesis: verum
end;
suppose a: x <> ColD1 . p ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A122: (firing_result (ColD0,ColD1,m,p)) . x = (m . p) . x by ;
A123: ((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by ;
((m . p) . x) + 0 <= ((m . p) . x) + 1 by XREAL_1:7;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 ) by ; :: thesis: verum
end;
end;
end;
suppose a: ( ( not p in (loc D0) \ (loc D1) or not t is_firable_on m,ColD0 ) & ( not p in (loc D1) \ (loc D0) or not t is_firable_on m,ColD0 ) ) ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 )
then A122: (firing_result (ColD0,ColD1,m,p)) . x = (m . p) . x by Def16;
A123: ((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by ;
((m . p) . x) + 0 <= ((m . p) . x) + 1 by XREAL_1:7;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= ((m . p) . x) + 1 ) by ; :: thesis: verum
end;
end;