defpred S_{1}[ 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_{1}[s,M . s] )
:: thesis: ( not t is_firable_at M0 implies ex b_{1} being marking of PTN st b_{1} = M0 )

thus ( t is_firable_at M0 implies ex M being marking of PTN st

for s being place of PTN holds S

proof

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

for s being place of PTN holds S_{1}[s,M . s]

A3: for x being Element of the carrier of PTN holds S_{1}[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_{1}[s,M . s]

thus for s being place of PTN holds S_{1}[s,M . s]
by A3; :: thesis: verum

end;for s being place of PTN holds S

A2: now :: thesis: for x being Element of PTN ex y being Element of NAT st S_{1}[x,y]

consider M being Function of the carrier of PTN,NAT such that let x be Element of PTN; :: thesis: ex y being Element of NAT st S_{1}[y,b_{2}]

end;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;

suppose S1:
( x in *' {t} & not x in {t} *' )
; :: thesis: ex y being Element of NAT st S_{1}[y,b_{2}]

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_{1}[x,M0x]
by S1;

hence ex y being Element of NAT st S_{1}[x,y]
; :: thesis: verum

end;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

hence ex y being Element of NAT st S

A3: for x being Element of the carrier of PTN holds S

reconsider M = M as marking of PTN by FUNCT_2:8;

take M ; :: thesis: for s being place of PTN holds S

thus for s being place of PTN holds S