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 )

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 ) ) )
;

end;

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;

end;A12: p in loc D0 by XBOOLE_0:def 5, A1;

per cases
( x = ColD0 . p or x <> ColD0 . p )
;

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 )

(((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;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

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;((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

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;((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