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 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 )
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 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 )
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 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 )
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 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 )
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 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 )
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 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 )
let ColD1 be color-threshold of D1; :: thesis: 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 )
let x be Element of the ColoredSet of CPN; :: thesis: 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 )
let p be Element of CPN; :: thesis: ( t is outbound implies ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x ) )
assume a: t is outbound ; :: thesis: ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x )

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 )

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 )

(((m . p) . x) - 1) + 0 <= (((m . p) . x) - 1) + 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 ) by a, A1, A11, A12, Def16Sub; :: 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 )

then A122: (firing_result (ColD0,ColD1,m,p)) . x = (m . p) . x by A1, A11, Def16Sub;
((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by A122, XREAL_1:13;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x ) by a, A1, A11, Def16Sub; :: thesis: verum

end;

end;

end;

suppose ( 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 )

hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x ) by a; :: thesis: verum

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 )

then A122: (firing_result (ColD0,ColD1,m,p)) . x = (m . p) . x by Def16;
((m . p) . x) - 1 <= ((firing_result (ColD0,ColD1,m,p)) . x) - 0 by A122, XREAL_1:13;
hence ( ((m . p) . x) - 1 <= (firing_result (ColD0,ColD1,m,p)) . x & (firing_result (ColD0,ColD1,m,p)) . x <= (m . p) . x ) by a, Def16; :: thesis: verum

end;

end;