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 XBOOLE_0:def 5, A1;

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 a, A11, A12, Def16Sub, A1; :: 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 A11, Def16Sub, A1;
A123: ((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by A122, XREAL_1:13;
((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 a, A123, A11, Def16Sub, A1; :: 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 XBOOLE_0:def 5, A2;

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 A11, A12, Def16Add;
(((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 A11, Def16Add;
A123: ((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by A122, XREAL_1:13;
((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 A123, a, A11, Def16Add; :: 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 A122, XREAL_1:13;
((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 a, A123, Def16; :: thesis: verum

end;

end;