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₁[ 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₁[M1] & S₁[M2] implies M1 = M2 ) :: thesis: ( not t is_firable_at M0 & M1 = M0 & M2 = M0 implies M1 = M2 )

proof

assume A4: ( t is_firable_at M0 & S₁[M1] & S₁[M2] ) ; :: thesis: M1 = M2
for x being object st x in the carrier of PTN holds
M1 . x = M2 . x

proof

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 ;

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} *' ) ) ;

suppose S1: ( x in *' {t} & not x in {t} *' ) ; :: thesis: M1 . x = M2 . x

hence M1 . x = (M0 . x) - 1 by A4
.= M2 . x by S1, A4 ;
:: thesis: verum

end;

suppose S2: ( x in {t} *' & not x in *' {t} ) ; :: thesis: M1 . x = M2 . x

hence M1 . x = (M0 . x) + 1 by A4
.= M2 . x by S2, A4 ;
:: thesis: verum

end;

suppose S3: ( ( x in *' {t} & x in {t} *' ) or ( not x in *' {t} & not x in {t} *' ) ) ; :: thesis: M1 . x = M2 . x

thus M1 . x = M1 . x1
.= M0 . x by S3, A4
.= M2 . x1 by S3, A4
.= M2 . x ; :: thesis: verum

end;

end;

end;

hence M1 = M2 by FUNCT_2:12; :: thesis: verum

end;

thus ( not t is_firable_at M0 & M0 = M1 & M0 = M2 implies M1 = M2 ) ; :: thesis: verum