( 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) )
_{1} 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

( b_{1} = Ptr_Sub (ColD,m,p) iff b_{1} = Ptr_Add (ColE,m,p) )
; :: thesis: verum

proof

hence
for b
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) )
; :: thesis: 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) ; :: thesis: verum

end;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) ; :: thesis: verum

( b