let M1, M2 be marking of PTN; :: thesis: ( ( t is_firable_at M0 & ( for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies M1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies M1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies M1 . s = M0 . s ) ) ) & ( for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies M2 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies M2 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies M2 . s = M0 . s ) ) ) implies M1 = M2 ) & ( not t is_firable_at M0 & M1 = M0 & M2 = M0 implies M1 = M2 ) )

defpred S_{1}[ marking of PTN] means for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies $1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies $1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies $1 . s = M0 . s ) );

thus ( t is_firable_at M0 & S_{1}[M1] & S_{1}[M2] implies M1 = M2 )
:: thesis: ( not t is_firable_at M0 & M1 = M0 & M2 = M0 implies M1 = M2 )

( ( s in *' {t} & not s in {t} *' implies M1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies M1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies M1 . s = M0 . s ) ) ) & ( for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies M2 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies M2 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies M2 . s = M0 . s ) ) ) implies M1 = M2 ) & ( not t is_firable_at M0 & M1 = M0 & M2 = M0 implies M1 = M2 ) )

defpred S

( ( s in *' {t} & not s in {t} *' implies $1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies $1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies $1 . s = M0 . s ) );

thus ( t is_firable_at M0 & S

proof

thus
( not t is_firable_at M0 & M0 = M1 & M0 = M2 implies M1 = M2 )
; :: thesis: verum
assume A4:
( t is_firable_at M0 & S_{1}[M1] & S_{1}[M2] )
; :: thesis: M1 = M2

for x being object st x in the carrier of PTN holds

M1 . x = M2 . x

end;for x being object st x in the carrier of PTN holds

M1 . x = M2 . x

proof

hence
M1 = M2
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of PTN implies M1 . x = M2 . x )

assume x in the carrier of PTN ; :: thesis: M1 . x = M2 . x

then reconsider x1 = x as place of PTN ;

end;assume x in the carrier of PTN ; :: thesis: M1 . x = M2 . x

then reconsider x1 = x as place of PTN ;

per cases
( ( x in *' {t} & not x in {t} *' ) or ( x in {t} *' & not x in *' {t} ) or ( x in *' {t} & x in {t} *' ) or ( not x in *' {t} & not x in {t} *' ) )
;

end;