let x be Element of the ColoredSet of CPN; :: thesis: ( ( p inloc D & x = ColD . p implies f . x =((m . p). x)+ 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f . x =(m . p). x ) )
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) )
byP2; hence
( ( p inloc D & x = ColD . p implies f . x =((m . p). x)+ 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f . x =(m . p). x ) )
; :: thesis: verum