defpred S1[ 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 S1[s,M . s] ) :: thesis: ( not t is_firable_at M0 implies ex b1 being marking of PTN st b1 = M0 )
proof
assume A1: t is_firable_at M0 ; :: thesis: ex M being marking of PTN st
for s being place of PTN holds S1[s,M . s]

A2: now :: thesis: for x being Element of PTN ex y being Element of NAT st S1[x,y]
let x be Element of PTN; :: thesis: ex y being Element of NAT st S1[y,b2]
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 S1[y,b2]
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 ;
then reconsider M0x = (M0 . x) - 1 as Element of NAT by ;
S1[x,M0x] by S1;
hence ex y being Element of NAT st S1[x,y] ; :: thesis: verum
end;
suppose ( x in {t} *' & not x in *' {t} ) ; :: thesis: ex y being Element of NAT st S1[y,b2]
hence ex y being Element of NAT st S1[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 S1[y,b2]
hence ex y being Element of NAT st S1[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 S1[x,M . x] from reconsider M = M as marking of PTN by FUNCT_2:8;
take M ; :: thesis: for s being place of PTN holds S1[s,M . s]
thus for s being place of PTN holds S1[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