defpred S₁[ place of PTN, set ] means ( ( $1 in *' {t} & not $1 in {t} *' implies $2 = (M0 . $1) - 1 ) & ( $1 in {t} *' & not $1 in *' {t} implies $2 = (M0 . $1) + 1 ) & ( ( ( $1 in *' {t} & $1 in {t} *' ) or ( not $1 in *' {t} & not $1 in {t} *' ) ) implies $2 = M0 . $1 ) );
thus ( t is_firable_at M0 implies ex M being marking of PTN st
for s being place of PTN holds S₁[s,M . s] ) :: thesis: ( not t is_firable_at M0 implies ex b₁ being marking of PTN st b₁ = M0 )

proof

assume A1: t is_firable_at M0 ; :: thesis: ex M being marking of PTN st
for s being place of PTN holds S₁[s,M . s]

A2: now :: thesis: for x being Element of PTN ex y being Element of NAT st S₁[x,y]

let x be Element of PTN; :: thesis: ex y being Element of NAT st S₁[y,b₂]

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: ex y being Element of NAT st S₁[y,b₂]

dom M0 = the carrier of PTN by FUNCT_2:def 1;
then [x,(M0 . x)] in M0 by FUNCT_1:def 2;
then M0 . x in M0 .: (*' {t}) by RELAT_1:def 13, S1;
then reconsider M0x = (M0 . x) - 1 as Element of NAT by NAT_1:20, A1;
S₁[x,M0x] by S1;
hence ex y being Element of NAT st S₁[x,y] ; :: thesis: verum

end;

suppose ( x in {t} *' & not x in *' {t} ) ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

hence ex y being Element of NAT st S₁[x,y] ; :: thesis: verum

end;

suppose ( ( x in *' {t} & x in {t} *' ) or ( not x in *' {t} & not x in {t} *' ) ) ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

hence ex y being Element of NAT st S₁[x,y] ; :: thesis: verum

end;

end;

end;

consider M being Function of the carrier of PTN,NAT such that
A3: for x being Element of the carrier of PTN holds S₁[x,M . x] from FUNCT_2:sch 3(A2);
reconsider M = M as marking of PTN by FUNCT_2:8;
take M ; :: thesis: for s being place of PTN holds S₁[s,M . s]
thus for s being place of PTN holds S₁[s,M . s] by A3; :: thesis: verum

end;

thus ( not t is_firable_at M0 implies ex M being marking of PTN st M = M0 ) ; :: thesis: verum