( t is_firable_on m,ColD & p in (loc D) \ (loc E) & t is_firable_on m,ColD & p in (loc E) \ (loc D) implies Ptr_Sub (ColD,m,p) = Ptr_Add (ColE,m,p) )
proof
assume
(
t is_firable_on m,
ColD &
p in (loc D) \ (loc E) &
t is_firable_on m,
ColD &
p in (loc E) \ (loc D) )
;
Ptr_Sub (ColD,m,p) = Ptr_Add (ColE,m,p)
then
(
p in loc D & not
p in loc D )
by XBOOLE_0:def 5;
hence
Ptr_Sub (
ColD,
m,
p)
= Ptr_Add (
ColE,
m,
p)
;
verum
end;
hence
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) )
; verum