let Dftn be Decision_free_PT; :: thesis: for dct being Circuit_of_places_and_trans of Dftn

for M0 being marking of Dftn

for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let dct be Circuit_of_places_and_trans of Dftn; :: thesis: for M0 being marking of Dftn

for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let M0 be marking of Dftn; :: thesis: for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let t be transition of Dftn; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

A65a: dct /^ 1 is one-to-one by JORDAN23:14;

set P = places_of dct;

A21: len dct >= 3 by Def5;

then 1 <= len dct by XXREAL_0:2;

then X1: 1 in dom dct by FINSEQ_3:25;

L2: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

L1: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;

then reconsider dct1 = dct . 1 as place of Dftn by ZFMISC_1:87;

dct1 in rng dct by FUNCT_1:3, X1;

then K23: dct . 1 in places_of dct ;

set pl = the Enumeration of places_of dct;

set FM0 = Firing (t,M0);

set mM0 = the Enumeration of M0, places_of dct;

set mFM0 = the Enumeration of Firing (t,M0), places_of dct;

for M0 being marking of Dftn

for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let dct be Circuit_of_places_and_trans of Dftn; :: thesis: for M0 being marking of Dftn

for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let M0 be marking of Dftn; :: thesis: for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let t be transition of Dftn; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

A65a: dct /^ 1 is one-to-one by JORDAN23:14;

set P = places_of dct;

A21: len dct >= 3 by Def5;

then 1 <= len dct by XXREAL_0:2;

then X1: 1 in dom dct by FINSEQ_3:25;

L2: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

L1: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;

then reconsider dct1 = dct . 1 as place of Dftn by ZFMISC_1:87;

dct1 in rng dct by FUNCT_1:3, X1;

then K23: dct . 1 in places_of dct ;

set pl = the Enumeration of places_of dct;

set FM0 = Firing (t,M0);

set mM0 = the Enumeration of M0, places_of dct;

set mFM0 = the Enumeration of Firing (t,M0), places_of dct;

per cases
( t is_firable_at M0 or not t is_firable_at M0 )
;

end;

suppose A10:
t is_firable_at M0
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

end;

per cases
( t in transitions_of dct or not t in transitions_of dct )
;

end;

suppose
t in transitions_of dct
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

then consider t1 being transition of Dftn such that

A46: ( t1 = t & t1 in rng dct ) ;

consider n being object such that

A47: ( n in dom dct & dct . n = t ) by FUNCT_1:def 3, A46;

G2: dct . n in transitions_of dct by A46, A47;

reconsider n = n as Element of NAT by A47;

K12: ( 1 <= n & n <= len dct ) by A47, FINSEQ_3:25;

K8: t in {t} by TARSKI:def 1;

end;A46: ( t1 = t & t1 in rng dct ) ;

consider n being object such that

A47: ( n in dom dct & dct . n = t ) by FUNCT_1:def 3, A46;

G2: dct . n in transitions_of dct by A46, A47;

reconsider n = n as Element of NAT by A47;

K12: ( 1 <= n & n <= len dct ) by A47, FINSEQ_3:25;

K8: t in {t} by TARSKI:def 1;

per cases
( len dct = 3 or len dct > 3 )
by A21, XXREAL_0:1;

end;

suppose K10:
len dct = 3
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

K13:
1 mod 2 = 1
by NAT_D:14;

(2 * 1) mod 2 = 0 by NAT_D:13;

then K14: (2 + 1) mod 2 = 1 by K13, NAT_D:17;

X4: n mod 2 = 0 by Thcc, G2, A47;

then ( n <> 1 & n <> 3 ) by NAT_D:14, K14;

then ( 1 < n & n < 3 ) by K12, K10, XXREAL_0:1;

then X5: 1 + 1 <= n by NAT_1:13;

n < 2 + 1 by K12, K10, XXREAL_0:1, K14, X4;

then n <= 2 by NAT_1:13;

then K7: t = dct . 2 by A47, XXREAL_0:1, X5;

K21: rng the Enumeration of places_of dct = {(dct . 1)}

then X7: len the Enumeration of places_of dct >= 0 + 1 by NAT_1:13;

A24: len the Enumeration of places_of dct = 1

A26: len the Enumeration of M0, places_of dct = 1 by Def12, A24, K23;

the Enumeration of places_of dct = <*(dct . 1)*> by FINSEQ_1:39, A24, K21;

then K9: the Enumeration of places_of dct . 1 = dct . 1 by FINSEQ_1:40;

reconsider pl1 = the Enumeration of places_of dct . 1 as place of Dftn by L1, ZFMISC_1:87, K9;

K11: the Enumeration of places_of dct . 1 = dct . 3 by K10, K9, Lm1;

consider f being S-T_arc of Dftn such that

K5: f = [pl1,t] by K7, K9, L1;

K4: pl1 in *' {t} by K5, K8;

consider g being T-S_arc of Dftn such that

K5a: g = [t,pl1] by K10, K7, K11, L2;

K4a: pl1 in {t} *' by K8, K5a;

K2: dom the Enumeration of M0, places_of dct = dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:29, A25, A26;

end;(2 * 1) mod 2 = 0 by NAT_D:13;

then K14: (2 + 1) mod 2 = 1 by K13, NAT_D:17;

X4: n mod 2 = 0 by Thcc, G2, A47;

then ( n <> 1 & n <> 3 ) by NAT_D:14, K14;

then ( 1 < n & n < 3 ) by K12, K10, XXREAL_0:1;

then X5: 1 + 1 <= n by NAT_1:13;

n < 2 + 1 by K12, K10, XXREAL_0:1, K14, X4;

then n <= 2 by NAT_1:13;

then K7: t = dct . 2 by A47, XXREAL_0:1, X5;

K21: rng the Enumeration of places_of dct = {(dct . 1)}

proof

the Enumeration of places_of dct <> {}
by K21;
thus
rng the Enumeration of places_of dct c= {(dct . 1)}
:: according to XBOOLE_0:def 10 :: thesis: {(dct . 1)} c= rng the Enumeration of places_of dct

assume x in {(dct . 1)} ; :: thesis: x in rng the Enumeration of places_of dct

then x = dct . 1 by TARSKI:def 1;

hence x in rng the Enumeration of places_of dct by RLAFFIN3:def 1, K23; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(dct . 1)} or x in rng the Enumeration of places_of dct )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Enumeration of places_of dct or x in {(dct . 1)} )

assume x in rng the Enumeration of places_of dct ; :: thesis: x in {(dct . 1)}

then x in places_of dct by RLAFFIN3:def 1;

then consider p being place of Dftn such that

K24: ( p = x & p in rng dct ) ;

consider y being object such that

K25: ( y in dom dct & dct . y = p ) by FUNCT_1:def 3, K24;

reconsider y = y as Element of NAT by K25;

K26: ( 1 <= y & y <= 3 ) by FINSEQ_3:25, K25, K10;

then ( 1 = y or 1 < y ) by XXREAL_0:1;

then X7: ( 1 = y or 1 + 1 <= y ) by NAT_1:13;

X6: ( 3 = y or y < 2 + 1 ) by K26, XXREAL_0:1;

K34: y <> 2 by XBOOLE_0:3, NET_1:def 2, K25, K7;

x = dct . 1 by K24, K25, NAT_1:22, X6, X7, K34, Lm1, K10;

hence x in {(dct . 1)} by TARSKI:def 1; :: thesis: verum

end;assume x in rng the Enumeration of places_of dct ; :: thesis: x in {(dct . 1)}

then x in places_of dct by RLAFFIN3:def 1;

then consider p being place of Dftn such that

K24: ( p = x & p in rng dct ) ;

consider y being object such that

K25: ( y in dom dct & dct . y = p ) by FUNCT_1:def 3, K24;

reconsider y = y as Element of NAT by K25;

K26: ( 1 <= y & y <= 3 ) by FINSEQ_3:25, K25, K10;

then ( 1 = y or 1 < y ) by XXREAL_0:1;

then X7: ( 1 = y or 1 + 1 <= y ) by NAT_1:13;

X6: ( 3 = y or y < 2 + 1 ) by K26, XXREAL_0:1;

K34: y <> 2 by XBOOLE_0:3, NET_1:def 2, K25, K7;

x = dct . 1 by K24, K25, NAT_1:22, X6, X7, K34, Lm1, K10;

hence x in {(dct . 1)} by TARSKI:def 1; :: thesis: verum

assume x in {(dct . 1)} ; :: thesis: x in rng the Enumeration of places_of dct

then x = dct . 1 by TARSKI:def 1;

hence x in rng the Enumeration of places_of dct by RLAFFIN3:def 1, K23; :: thesis: verum

then X7: len the Enumeration of places_of dct >= 0 + 1 by NAT_1:13;

A24: len the Enumeration of places_of dct = 1

proof

then A25:
len the Enumeration of Firing (t,M0), places_of dct = 1
by Def12, K23;
assume
len the Enumeration of places_of dct <> 1
; :: thesis: contradiction

then len the Enumeration of places_of dct > 1 by XXREAL_0:1, X7;

then len the Enumeration of places_of dct >= 1 + 1 by NAT_1:13;

then K47: 2 in dom the Enumeration of places_of dct by FINSEQ_3:25;

then K45: the Enumeration of places_of dct . 2 in rng the Enumeration of places_of dct by FUNCT_1:def 3;

K46: 1 in dom the Enumeration of places_of dct by X7, FINSEQ_3:25;

then K49: the Enumeration of places_of dct . 1 in rng the Enumeration of places_of dct by FUNCT_1:def 3;

the Enumeration of places_of dct . 2 = dct . 1 by TARSKI:def 1, K21, K45

.= the Enumeration of places_of dct . 1 by K21, K49, TARSKI:def 1 ;

hence contradiction by FUNCT_1:def 4, K46, K47; :: thesis: verum

end;then len the Enumeration of places_of dct > 1 by XXREAL_0:1, X7;

then len the Enumeration of places_of dct >= 1 + 1 by NAT_1:13;

then K47: 2 in dom the Enumeration of places_of dct by FINSEQ_3:25;

then K45: the Enumeration of places_of dct . 2 in rng the Enumeration of places_of dct by FUNCT_1:def 3;

K46: 1 in dom the Enumeration of places_of dct by X7, FINSEQ_3:25;

then K49: the Enumeration of places_of dct . 1 in rng the Enumeration of places_of dct by FUNCT_1:def 3;

the Enumeration of places_of dct . 2 = dct . 1 by TARSKI:def 1, K21, K45

.= the Enumeration of places_of dct . 1 by K21, K49, TARSKI:def 1 ;

hence contradiction by FUNCT_1:def 4, K46, K47; :: thesis: verum

A26: len the Enumeration of M0, places_of dct = 1 by Def12, A24, K23;

the Enumeration of places_of dct = <*(dct . 1)*> by FINSEQ_1:39, A24, K21;

then K9: the Enumeration of places_of dct . 1 = dct . 1 by FINSEQ_1:40;

reconsider pl1 = the Enumeration of places_of dct . 1 as place of Dftn by L1, ZFMISC_1:87, K9;

K11: the Enumeration of places_of dct . 1 = dct . 3 by K10, K9, Lm1;

consider f being S-T_arc of Dftn such that

K5: f = [pl1,t] by K7, K9, L1;

K4: pl1 in *' {t} by K5, K8;

consider g being T-S_arc of Dftn such that

K5a: g = [t,pl1] by K10, K7, K11, L2;

K4a: pl1 in {t} *' by K8, K5a;

K2: dom the Enumeration of M0, places_of dct = dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:29, A25, A26;

now :: thesis: for x being Element of NAT st x in dom the Enumeration of M0, places_of dct holds

the Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . x

hence
num_marks ((places_of dct),(Firing (t,M0))) = num_marks ((places_of dct),M0)
by PARTFUN1:5, K2; :: thesis: verumthe Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . x

let x be Element of NAT ; :: thesis: ( x in dom the Enumeration of M0, places_of dct implies the Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . x )

assume C13b: x in dom the Enumeration of M0, places_of dct ; :: thesis: the Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . x

then ( 1 <= x & x <= len the Enumeration of M0, places_of dct ) by FINSEQ_3:25;

then K3: x = 1 by NAT_1:25, A26;

hence the Enumeration of M0, places_of dct . x = M0 . pl1 by Def12, C13b, K23

.= (Firing (t,M0)) . pl1 by Def11, K4, A10, K4a

.= the Enumeration of Firing (t,M0), places_of dct . x by K2, C13b, Def12, K23, K3 ;

:: thesis: verum

end;assume C13b: x in dom the Enumeration of M0, places_of dct ; :: thesis: the Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . x

then ( 1 <= x & x <= len the Enumeration of M0, places_of dct ) by FINSEQ_3:25;

then K3: x = 1 by NAT_1:25, A26;

hence the Enumeration of M0, places_of dct . x = M0 . pl1 by Def12, C13b, K23

.= (Firing (t,M0)) . pl1 by Def11, K4, A10, K4a

.= the Enumeration of Firing (t,M0), places_of dct . x by K2, C13b, Def12, K23, K3 ;

:: thesis: verum

suppose A74:
len dct > 3
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

A81:
1 < len dct
by A74, XXREAL_0:2;

A53a: 1 <= n by FINSEQ_3:25, A47;

A53b: 2 < len dct by XXREAL_0:2, A74;

then A48: 1 + 1 <= n by NAT_1:13;

A80: 1 < n + 1 by A53a, NAT_1:16;

A53: n <= len dct by A47, FINSEQ_3:25;

then A82: n + 1 <= len dct by NAT_1:13;

reconsider nm1 = n - 1 as Element of NAT by FINSEQ_3:26, A47;

A78: 2 + (- 1) <= n + (- 1) by A48, XREAL_1:6;

A87: nm1 < len dct by XXREAL_0:2, A53, XREAL_1:146;

then G3: nm1 in dom dct by FINSEQ_3:25, A78;

A56: [(dct . nm1),(dct . n)] in the S-T_Arcs of Dftn by Thf, G2, A47;

[(dct . n),(dct . (n + 1))] in the T-S_Arcs of Dftn by Thf, G2, A47;

then reconsider q = dct . nm1, r = dct . (n + 1) as place of Dftn by ZFMISC_1:87, A56;

reconsider qt = [q,t] as S-T_arc of Dftn by Thf, G2, A47;

reconsider tr = [t,r] as T-S_arc of Dftn by Thf, G2, A47;

A50: q in rng dct by FUNCT_1:3, G3;

n + 1 in dom dct by FINSEQ_3:25, A80, A82;

then A50a: r in rng dct by FUNCT_1:3;

A57: q <> r

( not s in *' {t} & not s in {t} *' ) by E1;

E1cona: for s being place of Dftn st s in rng dct & s <> r & s <> q holds

( not s in *' {t} & not s in {t} *' ) by E1;

A59: qt = [q,t] ;

A58: t in {t} by TARSKI:def 1;

then A30a: ( q in *' {t} & not q in {t} *' ) by A59, A50, A57, E1;

A59a: tr = [t,r] ;

A30b: ( r in {t} *' & not r in *' {t} ) by A59a, A50a, A57, E1, A58;

set nq = q .. the Enumeration of places_of dct;

set nr = r .. the Enumeration of places_of dct;

set nqm1 = (q .. the Enumeration of places_of dct) -' 1;

set nrm1 = (r .. the Enumeration of places_of dct) -' 1;

A44: len the Enumeration of M0, places_of dct = len the Enumeration of places_of dct by Def12, K23

.= len the Enumeration of Firing (t,M0), places_of dct by Def12, K23 ;

q in places_of dct by A50;

then A32a: q in rng the Enumeration of places_of dct by RLAFFIN3:def 1;

r in places_of dct by A50a;

then A32: r in rng the Enumeration of places_of dct by RLAFFIN3:def 1;

end;A53a: 1 <= n by FINSEQ_3:25, A47;

A53b: 2 < len dct by XXREAL_0:2, A74;

now :: thesis: not 1 = n

then A62:
1 < n
by A53a, XXREAL_0:1;assume
1 = n
; :: thesis: contradiction

then dct . n in the carrier of Dftn by L1, ZFMISC_1:87;

hence contradiction by XBOOLE_0:3, NET_1:def 2, A47; :: thesis: verum

end;then dct . n in the carrier of Dftn by L1, ZFMISC_1:87;

hence contradiction by XBOOLE_0:3, NET_1:def 2, A47; :: thesis: verum

then A48: 1 + 1 <= n by NAT_1:13;

A80: 1 < n + 1 by A53a, NAT_1:16;

A53: n <= len dct by A47, FINSEQ_3:25;

now :: thesis: not n = len dct

then
n < len dct
by A53, XXREAL_0:1;assume
n = len dct
; :: thesis: contradiction

then dct . n in the carrier of Dftn by L2, ZFMISC_1:87;

hence contradiction by XBOOLE_0:3, NET_1:def 2, A47; :: thesis: verum

end;then dct . n in the carrier of Dftn by L2, ZFMISC_1:87;

hence contradiction by XBOOLE_0:3, NET_1:def 2, A47; :: thesis: verum

then A82: n + 1 <= len dct by NAT_1:13;

reconsider nm1 = n - 1 as Element of NAT by FINSEQ_3:26, A47;

A78: 2 + (- 1) <= n + (- 1) by A48, XREAL_1:6;

A87: nm1 < len dct by XXREAL_0:2, A53, XREAL_1:146;

then G3: nm1 in dom dct by FINSEQ_3:25, A78;

A56: [(dct . nm1),(dct . n)] in the S-T_Arcs of Dftn by Thf, G2, A47;

[(dct . n),(dct . (n + 1))] in the T-S_Arcs of Dftn by Thf, G2, A47;

then reconsider q = dct . nm1, r = dct . (n + 1) as place of Dftn by ZFMISC_1:87, A56;

reconsider qt = [q,t] as S-T_arc of Dftn by Thf, G2, A47;

reconsider tr = [t,r] as T-S_arc of Dftn by Thf, G2, A47;

A50: q in rng dct by FUNCT_1:3, G3;

n + 1 in dom dct by FINSEQ_3:25, A80, A82;

then A50a: r in rng dct by FUNCT_1:3;

A57: q <> r

proof

assume A79:
q = r
; :: thesis: contradiction

end;E1: now :: thesis: for s being place of Dftn st s in rng dct holds

( ( s <> r implies not s in {t} *' ) & ( s <> q implies not s in *' {t} ) )

E1con:
for s being place of Dftn st s in rng dct & s <> q & s <> r holds ( ( s <> r implies not s in {t} *' ) & ( s <> q implies not s in *' {t} ) )

let s be place of Dftn; :: thesis: ( s in rng dct implies ( ( s <> r implies not s in {t} *' ) & ( s <> q implies not s in *' {t} ) ) )

assume D9: s in rng dct ; :: thesis: ( ( s <> r implies not s in {t} *' ) & ( s <> q implies not s in *' {t} ) )

consider ns being object such that

D1: ( ns in dom dct & dct . ns = s ) by FUNCT_1:def 3, D9;

G5: dct . ns in places_of dct by D9, D1;

reconsider ns = ns as Element of NAT by D1;

D2: ( 1 <= ns & ns <= len dct ) by D1, FINSEQ_3:25;

thus ( s <> r implies not s in {t} *' ) :: thesis: ( s <> q implies not s in *' {t} )

end;assume D9: s in rng dct ; :: thesis: ( ( s <> r implies not s in {t} *' ) & ( s <> q implies not s in *' {t} ) )

consider ns being object such that

D1: ( ns in dom dct & dct . ns = s ) by FUNCT_1:def 3, D9;

G5: dct . ns in places_of dct by D9, D1;

reconsider ns = ns as Element of NAT by D1;

D2: ( 1 <= ns & ns <= len dct ) by D1, FINSEQ_3:25;

thus ( s <> r implies not s in {t} *' ) :: thesis: ( s <> q implies not s in *' {t} )

proof

thus
( s <> q implies not s in *' {t} )
:: thesis: verum
assume D10:
( s <> r & s in {t} *' )
; :: thesis: contradiction

then consider f being T-S_arc of Dftn, tt being transition of Dftn such that

A61: ( tt in {t} & f = [tt,s] ) by PETRI:8;

end;then consider f being T-S_arc of Dftn, tt being transition of Dftn such that

A61: ( tt in {t} & f = [tt,s] ) by PETRI:8;

per cases
( 1 = ns or ns = len dct or ( 1 < ns & ns < len dct ) )
by D2, XXREAL_0:1;

end;

suppose A72:
( 1 = ns or ns = len dct )
; :: thesis: contradiction

reconsider lm1 = (len dct) - 1 as Element of NAT by NAT_1:21, A21, XXREAL_0:2;

3 + (- 1) < (len dct) + (- 1) by A74, XREAL_1:8;

then D11: ( 1 < lm1 & lm1 <= len dct ) by XREAL_1:146, XXREAL_0:2;

[(dct . lm1),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

then consider g being Element of the T-S_Arcs of Dftn such that

A63a: g = [(dct . lm1),(dct . (len dct))] ;

reconsider t1 = dct . lm1 as transition of Dftn by ZFMISC_1:87, A63a;

g = [t1,s] by A63a, A72, Lm1, D1;

then dct . lm1 = tt by A61, Def1

.= dct . n by A47, TARSKI:def 1, A61 ;

then lm1 = n by A65a, Th10, D11, A62, A53;

hence contradiction by D10, D1, A72, Lm1; :: thesis: verum

end;3 + (- 1) < (len dct) + (- 1) by A74, XREAL_1:8;

then D11: ( 1 < lm1 & lm1 <= len dct ) by XREAL_1:146, XXREAL_0:2;

[(dct . lm1),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

then consider g being Element of the T-S_Arcs of Dftn such that

A63a: g = [(dct . lm1),(dct . (len dct))] ;

reconsider t1 = dct . lm1 as transition of Dftn by ZFMISC_1:87, A63a;

g = [t1,s] by A63a, A72, Lm1, D1;

then dct . lm1 = tt by A61, Def1

.= dct . n by A47, TARSKI:def 1, A61 ;

then lm1 = n by A65a, Th10, D11, A62, A53;

hence contradiction by D10, D1, A72, Lm1; :: thesis: verum

suppose D6:
( 1 < ns & ns < len dct )
; :: thesis: contradiction

then
1 + 1 <= ns
by NAT_1:13;

then reconsider nsm2 = ns - 2 as Element of NAT by NAT_1:21;

reconsider nsm1 = ns - 1 as Element of NAT by NAT_1:21, D6;

A63: [(dct . (ns - 1)),(dct . ns)] in the T-S_Arcs of Dftn by Thg, D6, G5;

reconsider g = [(dct . (ns - 1)),(dct . ns)] as Element of the T-S_Arcs of Dftn by Thg, D6, G5;

reconsider t1 = dct . (ns - 1) as transition of Dftn by ZFMISC_1:87, A63;

3 <= ns by Thg, D6, G5;

then 3 + (- 1) <= ns + (- 1) by XREAL_1:6;

then D8: ( 1 < ns - 1 & ns - 1 <= len dct ) by D6, XXREAL_0:2, XREAL_1:146;

g = [t1,s] by D1;

then dct . nsm1 = tt by A61, Def1

.= dct . n by A47, TARSKI:def 1, A61 ;

then dct . ((ns - 1) + 1) = dct . (n + 1) by A65a, Th10, D8, A62, A53;

hence contradiction by D1, D10; :: thesis: verum

end;then reconsider nsm2 = ns - 2 as Element of NAT by NAT_1:21;

reconsider nsm1 = ns - 1 as Element of NAT by NAT_1:21, D6;

A63: [(dct . (ns - 1)),(dct . ns)] in the T-S_Arcs of Dftn by Thg, D6, G5;

reconsider g = [(dct . (ns - 1)),(dct . ns)] as Element of the T-S_Arcs of Dftn by Thg, D6, G5;

reconsider t1 = dct . (ns - 1) as transition of Dftn by ZFMISC_1:87, A63;

3 <= ns by Thg, D6, G5;

then 3 + (- 1) <= ns + (- 1) by XREAL_1:6;

then D8: ( 1 < ns - 1 & ns - 1 <= len dct ) by D6, XXREAL_0:2, XREAL_1:146;

g = [t1,s] by D1;

then dct . nsm1 = tt by A61, Def1

.= dct . n by A47, TARSKI:def 1, A61 ;

then dct . ((ns - 1) + 1) = dct . (n + 1) by A65a, Th10, D8, A62, A53;

hence contradiction by D1, D10; :: thesis: verum

proof

assume D10a:
( s <> q & s in *' {t} )
; :: thesis: contradiction

then consider f being S-T_arc of Dftn, tt being transition of Dftn such that

A61b: ( tt in {t} & f = [s,tt] ) by PETRI:6;

end;then consider f being S-T_arc of Dftn, tt being transition of Dftn such that

A61b: ( tt in {t} & f = [s,tt] ) by PETRI:6;

per cases
( 1 = ns or ns = len dct or ( 1 < ns & ns < len dct ) )
by D2, XXREAL_0:1;

end;

suppose A72b:
( 1 = ns or ns = len dct )
; :: thesis: contradiction

[(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn
by Thd;

then consider g being Element of the S-T_Arcs of Dftn such that

A63b: g = [(dct . 1),(dct . 2)] ;

reconsider t1 = dct . 2 as transition of Dftn by ZFMISC_1:87, A63b;

g = [s,t1] by A63b, A72b, Lm1, D1;

then dct . 2 = tt by A61b, Def1

.= dct . n by A47, TARSKI:def 1, A61b ;

then 2 = n by A65a, Th10, A62, A53, A53b;

hence contradiction by D10a, A72b, Lm1, D1; :: thesis: verum

end;then consider g being Element of the S-T_Arcs of Dftn such that

A63b: g = [(dct . 1),(dct . 2)] ;

reconsider t1 = dct . 2 as transition of Dftn by ZFMISC_1:87, A63b;

g = [s,t1] by A63b, A72b, Lm1, D1;

then dct . 2 = tt by A61b, Def1

.= dct . n by A47, TARSKI:def 1, A61b ;

then 2 = n by A65a, Th10, A62, A53, A53b;

hence contradiction by D10a, A72b, Lm1, D1; :: thesis: verum

suppose D6:
( 1 < ns & ns < len dct )
; :: thesis: contradiction

then A63bb:
[(dct . ns),(dct . (ns + 1))] in the S-T_Arcs of Dftn
by Thg, G5;

reconsider g = [s,(dct . (ns + 1))] as Element of the S-T_Arcs of Dftn by Thg, G5, D1, D6;

reconsider t1 = dct . (ns + 1) as transition of Dftn by ZFMISC_1:87, A63bb;

D8: ( 1 < ns + 1 & ns + 1 <= len dct ) by D6, NAT_1:13;

g = [s,t1] ;

then dct . (ns + 1) = tt by A61b, Def1

.= dct . n by A47, TARSKI:def 1, A61b ;

then (ns + 1) - 1 = n - 1 by A65a, Th10, D8, A62, A53;

hence contradiction by D1, D10a; :: thesis: verum

end;reconsider g = [s,(dct . (ns + 1))] as Element of the S-T_Arcs of Dftn by Thg, G5, D1, D6;

reconsider t1 = dct . (ns + 1) as transition of Dftn by ZFMISC_1:87, A63bb;

D8: ( 1 < ns + 1 & ns + 1 <= len dct ) by D6, NAT_1:13;

g = [s,t1] ;

then dct . (ns + 1) = tt by A61b, Def1

.= dct . n by A47, TARSKI:def 1, A61b ;

then (ns + 1) - 1 = n - 1 by A65a, Th10, D8, A62, A53;

hence contradiction by D1, D10a; :: thesis: verum

( not s in *' {t} & not s in {t} *' ) by E1;

E1cona: for s being place of Dftn st s in rng dct & s <> r & s <> q holds

( not s in *' {t} & not s in {t} *' ) by E1;

A59: qt = [q,t] ;

A58: t in {t} by TARSKI:def 1;

then A30a: ( q in *' {t} & not q in {t} *' ) by A59, A50, A57, E1;

A59a: tr = [t,r] ;

A30b: ( r in {t} *' & not r in *' {t} ) by A59a, A50a, A57, E1, A58;

set nq = q .. the Enumeration of places_of dct;

set nr = r .. the Enumeration of places_of dct;

set nqm1 = (q .. the Enumeration of places_of dct) -' 1;

set nrm1 = (r .. the Enumeration of places_of dct) -' 1;

A44: len the Enumeration of M0, places_of dct = len the Enumeration of places_of dct by Def12, K23

.= len the Enumeration of Firing (t,M0), places_of dct by Def12, K23 ;

q in places_of dct by A50;

then A32a: q in rng the Enumeration of places_of dct by RLAFFIN3:def 1;

r in places_of dct by A50a;

then A32: r in rng the Enumeration of places_of dct by RLAFFIN3:def 1;

gen: now :: thesis: for n1, n2 being Element of NAT

for p1, p2 being place of Dftn st n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct & n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) holds

num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

q .. the Enumeration of places_of dct <> r .. the Enumeration of places_of dct
for p1, p2 being place of Dftn st n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct & n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) holds

num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let n1, n2 be Element of NAT ; :: thesis: for p1, p2 being place of Dftn st n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct & n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) holds

num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let p1, p2 be place of Dftn; :: thesis: ( n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct & n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) implies num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0))) )

assume L3: ( n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct ) ; :: thesis: ( n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) implies num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0))) )

set n2m1 = n2 -' 1;

set n1m1 = n1 -' 1;

assume that

S1: n2 > n1 and

A32a: p1 in rng the Enumeration of places_of dct and

A32: p2 in rng the Enumeration of places_of dct and

L4: for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) and

L5: ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) ; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

A39a: n2 in dom the Enumeration of places_of dct by FINSEQ_4:20, A32, L3;

then A40: ( 1 <= n2 & n2 <= len the Enumeration of places_of dct ) by FINSEQ_3:25;

then A36: n2 <= len the Enumeration of M0, places_of dct by Def12, K23;

then A41: n2 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, A40;

A43: n2 -' 1 < n2 by XREAL_1:237, FINSEQ_3:25, A39a;

C18a: p2 = the Enumeration of places_of dct . n2 by FINSEQ_4:19, A32, L3;

C18: p1 = the Enumeration of places_of dct . n1 by FINSEQ_4:19, A32a, L3;

A39: n1 in dom the Enumeration of places_of dct by FINSEQ_4:20, A32a, L3;

then A37: 1 <= n1 by FINSEQ_3:25;

C19: n1 <= len the Enumeration of places_of dct by A39, FINSEQ_3:25;

C11: n1 -' 1 < n1 by XREAL_1:237, FINSEQ_3:25, A39;

X12: (n2 -' 1) + 1 > n1 by XREAL_1:235, FINSEQ_3:25, A39a, S1;

then A35: n2 -' 1 >= n1 by NAT_1:13;

then C4: n1 -' 1 < n2 -' 1 by XXREAL_0:2, C11;

set mM0b2 = the Enumeration of M0, places_of dct | (n2 -' 1);

set mFM0b2 = the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1);

A27: the Enumeration of M0, places_of dct = (( the Enumeration of M0, places_of dct | (n2 -' 1)) ^ <*( the Enumeration of M0, places_of dct . n2)*>) ^ ( the Enumeration of M0, places_of dct /^ n2) by FINSEQ_5:84, A36, A40

.= (( the Enumeration of M0, places_of dct | (n2 -' 1)) ^ <*( the Enumeration of M0, places_of dct /. n2)*>) ^ ( the Enumeration of M0, places_of dct /^ n2) by PARTFUN1:def 6, A41 ;

A36a: n2 <= len the Enumeration of Firing (t,M0), places_of dct by Def12, K23, A40;

then A41a: n2 in dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:25, A40;

A27a: the Enumeration of Firing (t,M0), places_of dct = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct . n2)*>) ^ ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by FINSEQ_5:84, A36a, A40

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>) ^ ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by PARTFUN1:def 6, A41a ;

F1: n2 -' 1 <= len the Enumeration of M0, places_of dct by A36, A43, XXREAL_0:2;

A42: len ( the Enumeration of M0, places_of dct | (n2 -' 1)) = n2 -' 1 by FINSEQ_1:59, A36, A43, XXREAL_0:2;

A42a: len ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) = n2 -' 1 by FINSEQ_1:59, A36a, A43, XXREAL_0:2;

A33a: n1 <= len ( the Enumeration of M0, places_of dct | (n2 -' 1)) by A35, FINSEQ_1:59, A36, A43, XXREAL_0:2;

A33: n1 <= len ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) by NAT_1:13, X12, A42a;

then A34: n1 in dom ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) by FINSEQ_3:25, A37;

A34a: n1 in dom ( the Enumeration of M0, places_of dct | (n2 -' 1)) by FINSEQ_3:25, A33a, A37;

n1 <= len the Enumeration of Firing (t,M0), places_of dct by S1, A36a, XXREAL_0:2;

then A31: n1 in dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:25, A37;

C12: n1 < len the Enumeration of M0, places_of dct by XXREAL_0:2, A36, S1;

then A31b: n1 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, A37;

G1: the Enumeration of M0, places_of dct | (n2 -' 1) = ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) . n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_5:84, A33a, A37

.= ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) by PARTFUN1:def 6, A34a ;

G2: the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1) = ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_5:84, A33, A37

.= ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by PARTFUN1:def 6, A34 ;

A29f: (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)

.= ((Sum (((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= (((Sum ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of M0, places_of dct /. n2)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of M0, places_of dct /. n2)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by A29, A29b, A29c, A29f

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:73

.= (((Sum ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= ((Sum (((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= (Sum ((((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= num_marks ((places_of dct),(Firing (t,M0))) by RVSUM_1:75, A27a, G2 ; :: thesis: verum

end;( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) holds

num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

let p1, p2 be place of Dftn; :: thesis: ( n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct & n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) implies num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0))) )

assume L3: ( n2 = p2 .. the Enumeration of places_of dct & n1 = p1 .. the Enumeration of places_of dct ) ; :: thesis: ( n2 > n1 & p1 in rng the Enumeration of places_of dct & p2 in rng the Enumeration of places_of dct & ( for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) ) & ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) implies num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0))) )

set n2m1 = n2 -' 1;

set n1m1 = n1 -' 1;

assume that

S1: n2 > n1 and

A32a: p1 in rng the Enumeration of places_of dct and

A32: p2 in rng the Enumeration of places_of dct and

L4: for s being place of Dftn st s in rng dct & s <> p2 & s <> p1 holds

( not s in *' {t} & not s in {t} *' ) and

L5: ( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) ) ; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

A39a: n2 in dom the Enumeration of places_of dct by FINSEQ_4:20, A32, L3;

then A40: ( 1 <= n2 & n2 <= len the Enumeration of places_of dct ) by FINSEQ_3:25;

then A36: n2 <= len the Enumeration of M0, places_of dct by Def12, K23;

then A41: n2 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, A40;

A43: n2 -' 1 < n2 by XREAL_1:237, FINSEQ_3:25, A39a;

C18a: p2 = the Enumeration of places_of dct . n2 by FINSEQ_4:19, A32, L3;

C18: p1 = the Enumeration of places_of dct . n1 by FINSEQ_4:19, A32a, L3;

A39: n1 in dom the Enumeration of places_of dct by FINSEQ_4:20, A32a, L3;

then A37: 1 <= n1 by FINSEQ_3:25;

C19: n1 <= len the Enumeration of places_of dct by A39, FINSEQ_3:25;

C11: n1 -' 1 < n1 by XREAL_1:237, FINSEQ_3:25, A39;

X12: (n2 -' 1) + 1 > n1 by XREAL_1:235, FINSEQ_3:25, A39a, S1;

then A35: n2 -' 1 >= n1 by NAT_1:13;

then C4: n1 -' 1 < n2 -' 1 by XXREAL_0:2, C11;

set mM0b2 = the Enumeration of M0, places_of dct | (n2 -' 1);

set mFM0b2 = the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1);

A27: the Enumeration of M0, places_of dct = (( the Enumeration of M0, places_of dct | (n2 -' 1)) ^ <*( the Enumeration of M0, places_of dct . n2)*>) ^ ( the Enumeration of M0, places_of dct /^ n2) by FINSEQ_5:84, A36, A40

.= (( the Enumeration of M0, places_of dct | (n2 -' 1)) ^ <*( the Enumeration of M0, places_of dct /. n2)*>) ^ ( the Enumeration of M0, places_of dct /^ n2) by PARTFUN1:def 6, A41 ;

A36a: n2 <= len the Enumeration of Firing (t,M0), places_of dct by Def12, K23, A40;

then A41a: n2 in dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:25, A40;

A27a: the Enumeration of Firing (t,M0), places_of dct = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct . n2)*>) ^ ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by FINSEQ_5:84, A36a, A40

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>) ^ ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by PARTFUN1:def 6, A41a ;

F1: n2 -' 1 <= len the Enumeration of M0, places_of dct by A36, A43, XXREAL_0:2;

A42: len ( the Enumeration of M0, places_of dct | (n2 -' 1)) = n2 -' 1 by FINSEQ_1:59, A36, A43, XXREAL_0:2;

A42a: len ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) = n2 -' 1 by FINSEQ_1:59, A36a, A43, XXREAL_0:2;

A33a: n1 <= len ( the Enumeration of M0, places_of dct | (n2 -' 1)) by A35, FINSEQ_1:59, A36, A43, XXREAL_0:2;

A33: n1 <= len ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) by NAT_1:13, X12, A42a;

then A34: n1 in dom ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) by FINSEQ_3:25, A37;

A34a: n1 in dom ( the Enumeration of M0, places_of dct | (n2 -' 1)) by FINSEQ_3:25, A33a, A37;

n1 <= len the Enumeration of Firing (t,M0), places_of dct by S1, A36a, XXREAL_0:2;

then A31: n1 in dom the Enumeration of Firing (t,M0), places_of dct by FINSEQ_3:25, A37;

C12: n1 < len the Enumeration of M0, places_of dct by XXREAL_0:2, A36, S1;

then A31b: n1 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, A37;

G1: the Enumeration of M0, places_of dct | (n2 -' 1) = ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) . n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_5:84, A33a, A37

.= ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) by PARTFUN1:def 6, A34a ;

G2: the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1) = ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_5:84, A33, A37

.= ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by PARTFUN1:def 6, A34 ;

A29f: (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)

proof

A29:
( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1) = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)
A29g: ( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1 =
( the Enumeration of M0, places_of dct | (n2 -' 1)) . n1
by PARTFUN1:def 6, A34a

.= the Enumeration of M0, places_of dct . n1 by FINSEQ_3:112, A35

.= M0 . ( the Enumeration of places_of dct . n1) by K23, Def12, A31b

.= M0 . p1 by FINSEQ_4:19, A32a, L3 ;

A29h: (Firing (t,M0)) . p1 = (Firing (t,M0)) . ( the Enumeration of places_of dct . n1) by FINSEQ_4:19, A32a, L3

.= the Enumeration of Firing (t,M0), places_of dct . n1 by K23, Def12, A31

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . n1 by FINSEQ_3:112, A35

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1 by PARTFUN1:def 6, A34 ;

A29i: the Enumeration of M0, places_of dct /. n2 = the Enumeration of M0, places_of dct . n2 by PARTFUN1:def 6, A41

.= M0 . ( the Enumeration of places_of dct . n2) by K23, Def12, A41

.= M0 . p2 by FINSEQ_4:19, A32, L3 ;

A29j: (Firing (t,M0)) . p2 = (Firing (t,M0)) . ( the Enumeration of places_of dct . n2) by FINSEQ_4:19, A32, L3

.= the Enumeration of Firing (t,M0), places_of dct . n2 by K23, Def12, A41a

.= the Enumeration of Firing (t,M0), places_of dct /. n2 by PARTFUN1:def 6, A41a ;

end;.= the Enumeration of M0, places_of dct . n1 by FINSEQ_3:112, A35

.= M0 . ( the Enumeration of places_of dct . n1) by K23, Def12, A31b

.= M0 . p1 by FINSEQ_4:19, A32a, L3 ;

A29h: (Firing (t,M0)) . p1 = (Firing (t,M0)) . ( the Enumeration of places_of dct . n1) by FINSEQ_4:19, A32a, L3

.= the Enumeration of Firing (t,M0), places_of dct . n1 by K23, Def12, A31

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . n1 by FINSEQ_3:112, A35

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1 by PARTFUN1:def 6, A34 ;

A29i: the Enumeration of M0, places_of dct /. n2 = the Enumeration of M0, places_of dct . n2 by PARTFUN1:def 6, A41

.= M0 . ( the Enumeration of places_of dct . n2) by K23, Def12, A41

.= M0 . p2 by FINSEQ_4:19, A32, L3 ;

A29j: (Firing (t,M0)) . p2 = (Firing (t,M0)) . ( the Enumeration of places_of dct . n2) by FINSEQ_4:19, A32, L3

.= the Enumeration of Firing (t,M0), places_of dct . n2 by K23, Def12, A41a

.= the Enumeration of Firing (t,M0), places_of dct /. n2 by PARTFUN1:def 6, A41a ;

per cases
( ( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} ) or ( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} ) )
by L5;

end;

suppose A29k:
( p2 in *' {t} & not p2 in {t} *' & p1 in {t} *' & not p1 in *' {t} )
; :: thesis: (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)

A29m:
(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1 = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1
by A29h, Def11, A29k, A10, A29g;

( the Enumeration of M0, places_of dct /. n2) - 1 = the Enumeration of Firing (t,M0), places_of dct /. n2 by A29j, A29i, Def11, A29k, A10;

hence (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2) by A29m; :: thesis: verum

end;( the Enumeration of M0, places_of dct /. n2) - 1 = the Enumeration of Firing (t,M0), places_of dct /. n2 by A29j, A29i, Def11, A29k, A10;

hence (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2) by A29m; :: thesis: verum

suppose A29l:
( p1 in *' {t} & not p1 in {t} *' & p2 in {t} *' & not p2 in *' {t} )
; :: thesis: (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)

A29n:
(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) - 1 = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1
by A29h, Def11, A29l, A10, A29g;

( the Enumeration of M0, places_of dct /. n2) + 1 = the Enumeration of Firing (t,M0), places_of dct /. n2 by A29j, Def11, A29l, A10, A29i;

hence (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2) by A29n; :: thesis: verum

end;( the Enumeration of M0, places_of dct /. n2) + 1 = the Enumeration of Firing (t,M0), places_of dct /. n2 by A29j, Def11, A29l, A10, A29i;

hence (((( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1) + 1) + ( the Enumeration of M0, places_of dct /. n2)) - 1 = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1) + ( the Enumeration of Firing (t,M0), places_of dct /. n2) by A29n; :: thesis: verum

proof

A29b:
( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1 = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1
n1 -' 1 <= len ( the Enumeration of M0, places_of dct | (n2 -' 1))
by FINSEQ_1:59, A36, A43, XXREAL_0:2, C4;

then C6: len (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) = n1 -' 1 by FINSEQ_1:59;

len (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) = n1 -' 1 by FINSEQ_1:59, A42a, C11, XXREAL_0:2, A35;

then C1: dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) = dom (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) by FINSEQ_3:29, C6;

end;then C6: len (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) = n1 -' 1 by FINSEQ_1:59;

len (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) = n1 -' 1 by FINSEQ_1:59, A42a, C11, XXREAL_0:2, A35;

then C1: dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) = dom (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) by FINSEQ_3:29, C6;

now :: thesis: for x being Element of NAT st x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) holds

(( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x

hence
( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1) = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)
by PARTFUN1:5, C1; :: thesis: verum(( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x

let x be Element of NAT ; :: thesis: ( x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) implies (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x )

assume C13: x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ; :: thesis: (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x

then C5: x <= n1 -' 1 by C6, FINSEQ_3:25;

then C17: x < n1 by XXREAL_0:2, C11;

then C20: ( 1 <= x & x <= len the Enumeration of M0, places_of dct ) by C12, XXREAL_0:2, C13, FINSEQ_3:25;

then C10: x in dom the Enumeration of M0, places_of dct by FINSEQ_3:25;

C10a: x in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C20;

x <= len the Enumeration of places_of dct by C17, C19, XXREAL_0:2;

then C21: x in dom the Enumeration of places_of dct by FINSEQ_3:25, C20;

then the Enumeration of places_of dct . x in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . x in places_of dct by RLAFFIN3:def 1;

then consider plx being place of Dftn such that

C15: ( plx = the Enumeration of places_of dct . x & plx in rng dct ) ;

C16: plx <> p1 by FUNCT_1:def 4, C5, C11, A39, C18, C21, C15;

plx <> p2 by FUNCT_1:def 4, A39a, C18a, C21, C15, C17, S1;

then C14: ( not plx in *' {t} & not plx in {t} *' ) by L4, C15, C16;

thus (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = ( the Enumeration of M0, places_of dct | (n2 -' 1)) . x by FINSEQ_3:112, C5

.= the Enumeration of M0, places_of dct . x by FINSEQ_3:112, XXREAL_0:2, C4, C5

.= M0 . plx by K23, Def12, C15, C10

.= (Firing (t,M0)) . plx by Def11, C14, A10

.= the Enumeration of Firing (t,M0), places_of dct . x by K23, Def12, C10a, C15

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . x by FINSEQ_3:112, XXREAL_0:2, C4, C5

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x by FINSEQ_3:112, C5 ; :: thesis: verum

end;assume C13: x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ; :: thesis: (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x

then C5: x <= n1 -' 1 by C6, FINSEQ_3:25;

then C17: x < n1 by XXREAL_0:2, C11;

then C20: ( 1 <= x & x <= len the Enumeration of M0, places_of dct ) by C12, XXREAL_0:2, C13, FINSEQ_3:25;

then C10: x in dom the Enumeration of M0, places_of dct by FINSEQ_3:25;

C10a: x in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C20;

x <= len the Enumeration of places_of dct by C17, C19, XXREAL_0:2;

then C21: x in dom the Enumeration of places_of dct by FINSEQ_3:25, C20;

then the Enumeration of places_of dct . x in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . x in places_of dct by RLAFFIN3:def 1;

then consider plx being place of Dftn such that

C15: ( plx = the Enumeration of places_of dct . x & plx in rng dct ) ;

C16: plx <> p1 by FUNCT_1:def 4, C5, C11, A39, C18, C21, C15;

plx <> p2 by FUNCT_1:def 4, A39a, C18a, C21, C15, C17, S1;

then C14: ( not plx in *' {t} & not plx in {t} *' ) by L4, C15, C16;

thus (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) . x = ( the Enumeration of M0, places_of dct | (n2 -' 1)) . x by FINSEQ_3:112, C5

.= the Enumeration of M0, places_of dct . x by FINSEQ_3:112, XXREAL_0:2, C4, C5

.= M0 . plx by K23, Def12, C15, C10

.= (Firing (t,M0)) . plx by Def11, C14, A10

.= the Enumeration of Firing (t,M0), places_of dct . x by K23, Def12, C10a, C15

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . x by FINSEQ_3:112, XXREAL_0:2, C4, C5

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) . x by FINSEQ_3:112, C5 ; :: thesis: verum

proof

A29c:
the Enumeration of M0, places_of dct /^ n2 = the Enumeration of Firing (t,M0), places_of dct /^ n2
C6b:
len (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) = (n2 -' 1) - n1
by RFINSEQ:def 1, A42, A35;

len (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) = (n2 -' 1) - n1 by RFINSEQ:def 1, A35, A42a;

then C1b: dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) = dom (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_3:29, C6b;

end;len (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) = (n2 -' 1) - n1 by RFINSEQ:def 1, A35, A42a;

then C1b: dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) = dom (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) by FINSEQ_3:29, C6b;

now :: thesis: for x being Element of NAT st x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) holds

(( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x

hence
( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1 = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1
by PARTFUN1:5, C1b; :: thesis: verum(( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x

let x be Element of NAT ; :: thesis: ( x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) implies (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x )

assume C13b: x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) ; :: thesis: (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x

then C18b: ( 1 <= x & x <= len (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) ) by FINSEQ_3:25;

then C17b: 1 + 0 <= x + n1 by XREAL_1:7;

X13: x + n1 <= (len (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1)) + n1 by XREAL_1:6, C18b;

then X14: x + n1 <= len the Enumeration of M0, places_of dct by F1, XXREAL_0:2, C6b;

then C10b: x + n1 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, C17b;

C10bb: x + n1 in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C17b, X14;

x + n1 < n2 by XXREAL_0:2, A43, C6b, X13;

then x + n1 <= len the Enumeration of places_of dct by A40, XXREAL_0:2;

then C21b: x + n1 in dom the Enumeration of places_of dct by FINSEQ_3:25, C17b;

then the Enumeration of places_of dct . (x + n1) in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . (x + n1) in places_of dct by RLAFFIN3:def 1;

then consider plxpn1 being place of Dftn such that

C15b: ( plxpn1 = the Enumeration of places_of dct . (x + n1) & plxpn1 in rng dct ) ;

C16b: plxpn1 <> p2 by FUNCT_1:def 4, A39a, C18a, C21b, C15b, A43, C6b, X13;

n1 + 0 < n1 + x by XREAL_1:29, C18b;

then plxpn1 <> p1 by FUNCT_1:def 4, A39, C18, C21b, C15b;

then C14b: ( not plxpn1 in *' {t} & not plxpn1 in {t} *' ) by L4, C16b, C15b;

thus (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = ( the Enumeration of M0, places_of dct | (n2 -' 1)) . (x + n1) by RFINSEQ:def 1, C13b, A33a

.= the Enumeration of M0, places_of dct . (x + n1) by FINSEQ_3:112, C6b, X13

.= M0 . plxpn1 by K23, Def12, C15b, C10b

.= (Firing (t,M0)) . plxpn1 by Def11, C14b, A10

.= the Enumeration of Firing (t,M0), places_of dct . (x + n1) by K23, Def12, C10bb, C15b

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . (x + n1) by FINSEQ_3:112, C6b, X13

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x by RFINSEQ:def 1, C13b, C1b, A33 ; :: thesis: verum

end;assume C13b: x in dom (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) ; :: thesis: (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x

then C18b: ( 1 <= x & x <= len (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) ) by FINSEQ_3:25;

then C17b: 1 + 0 <= x + n1 by XREAL_1:7;

X13: x + n1 <= (len (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1)) + n1 by XREAL_1:6, C18b;

then X14: x + n1 <= len the Enumeration of M0, places_of dct by F1, XXREAL_0:2, C6b;

then C10b: x + n1 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, C17b;

C10bb: x + n1 in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C17b, X14;

x + n1 < n2 by XXREAL_0:2, A43, C6b, X13;

then x + n1 <= len the Enumeration of places_of dct by A40, XXREAL_0:2;

then C21b: x + n1 in dom the Enumeration of places_of dct by FINSEQ_3:25, C17b;

then the Enumeration of places_of dct . (x + n1) in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . (x + n1) in places_of dct by RLAFFIN3:def 1;

then consider plxpn1 being place of Dftn such that

C15b: ( plxpn1 = the Enumeration of places_of dct . (x + n1) & plxpn1 in rng dct ) ;

C16b: plxpn1 <> p2 by FUNCT_1:def 4, A39a, C18a, C21b, C15b, A43, C6b, X13;

n1 + 0 < n1 + x by XREAL_1:29, C18b;

then plxpn1 <> p1 by FUNCT_1:def 4, A39, C18, C21b, C15b;

then C14b: ( not plxpn1 in *' {t} & not plxpn1 in {t} *' ) by L4, C16b, C15b;

thus (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = ( the Enumeration of M0, places_of dct | (n2 -' 1)) . (x + n1) by RFINSEQ:def 1, C13b, A33a

.= the Enumeration of M0, places_of dct . (x + n1) by FINSEQ_3:112, C6b, X13

.= M0 . plxpn1 by K23, Def12, C15b, C10b

.= (Firing (t,M0)) . plxpn1 by Def11, C14b, A10

.= the Enumeration of Firing (t,M0), places_of dct . (x + n1) by K23, Def12, C10bb, C15b

.= ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) . (x + n1) by FINSEQ_3:112, C6b, X13

.= (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . x by RFINSEQ:def 1, C13b, C1b, A33 ; :: thesis: verum

proof

thus num_marks ((places_of dct),M0) =
(Sum ((((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1)) ^ <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2))
by RVSUM_1:75, G1, A27
C6c:
len ( the Enumeration of M0, places_of dct /^ n2) = (len the Enumeration of M0, places_of dct) - n2
by RFINSEQ:def 1, A36;

len ( the Enumeration of Firing (t,M0), places_of dct /^ n2) = (len the Enumeration of Firing (t,M0), places_of dct) - n2 by RFINSEQ:def 1, A36a;

then C1c: dom ( the Enumeration of M0, places_of dct /^ n2) = dom ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by FINSEQ_3:29, A44, C6c;

end;len ( the Enumeration of Firing (t,M0), places_of dct /^ n2) = (len the Enumeration of Firing (t,M0), places_of dct) - n2 by RFINSEQ:def 1, A36a;

then C1c: dom ( the Enumeration of M0, places_of dct /^ n2) = dom ( the Enumeration of Firing (t,M0), places_of dct /^ n2) by FINSEQ_3:29, A44, C6c;

now :: thesis: for x being Element of NAT st x in dom ( the Enumeration of M0, places_of dct /^ n2) holds

( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x

hence
the Enumeration of M0, places_of dct /^ n2 = the Enumeration of Firing (t,M0), places_of dct /^ n2
by PARTFUN1:5, C1c; :: thesis: verum( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x

let x be Element of NAT ; :: thesis: ( x in dom ( the Enumeration of M0, places_of dct /^ n2) implies ( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x )

assume C13c: x in dom ( the Enumeration of M0, places_of dct /^ n2) ; :: thesis: ( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x

then C18c: ( 1 <= x & x <= len ( the Enumeration of M0, places_of dct /^ n2) ) by FINSEQ_3:25;

then C17c: 1 + 0 <= x + n2 by XREAL_1:7;

X15: x + n2 <= (len ( the Enumeration of M0, places_of dct /^ n2)) + n2 by XREAL_1:6, C18c;

then C10cc: x + n2 in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C17c, C6c;

C10c: x + n2 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, C17c, C6c, X15;

C22: x + n2 > n2 by XREAL_1:29, C18c;

x + n2 <= len the Enumeration of places_of dct by Def12, K23, C6c, X15;

then C21c: x + n2 in dom the Enumeration of places_of dct by FINSEQ_3:25, C17c;

then the Enumeration of places_of dct . (x + n2) in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . (x + n2) in places_of dct by RLAFFIN3:def 1;

then consider plxpn2 being place of Dftn such that

C15c: ( plxpn2 = the Enumeration of places_of dct . (x + n2) & plxpn2 in rng dct ) ;

C16c: plxpn2 <> p2 by FUNCT_1:def 4, A39a, C18a, C21c, C15c, C22;

n1 + 0 < n2 + x by XREAL_1:8, S1;

then plxpn2 <> p1 by FUNCT_1:def 4, A39, C18, C21c, C15c;

then C14c: ( not plxpn2 in *' {t} & not plxpn2 in {t} *' ) by L4, C16c, C15c;

thus ( the Enumeration of M0, places_of dct /^ n2) . x = the Enumeration of M0, places_of dct . (x + n2) by RFINSEQ:def 1, A36, C13c

.= M0 . plxpn2 by K23, Def12, C15c, C10c

.= (Firing (t,M0)) . plxpn2 by Def11, C14c, A10

.= the Enumeration of Firing (t,M0), places_of dct . (x + n2) by K23, Def12, C10cc, C15c

.= ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x by RFINSEQ:def 1, C13c, C1c, A36a ; :: thesis: verum

end;assume C13c: x in dom ( the Enumeration of M0, places_of dct /^ n2) ; :: thesis: ( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x

then C18c: ( 1 <= x & x <= len ( the Enumeration of M0, places_of dct /^ n2) ) by FINSEQ_3:25;

then C17c: 1 + 0 <= x + n2 by XREAL_1:7;

X15: x + n2 <= (len ( the Enumeration of M0, places_of dct /^ n2)) + n2 by XREAL_1:6, C18c;

then C10cc: x + n2 in dom the Enumeration of Firing (t,M0), places_of dct by A44, FINSEQ_3:25, C17c, C6c;

C10c: x + n2 in dom the Enumeration of M0, places_of dct by FINSEQ_3:25, C17c, C6c, X15;

C22: x + n2 > n2 by XREAL_1:29, C18c;

x + n2 <= len the Enumeration of places_of dct by Def12, K23, C6c, X15;

then C21c: x + n2 in dom the Enumeration of places_of dct by FINSEQ_3:25, C17c;

then the Enumeration of places_of dct . (x + n2) in rng the Enumeration of places_of dct by FUNCT_1:3;

then the Enumeration of places_of dct . (x + n2) in places_of dct by RLAFFIN3:def 1;

then consider plxpn2 being place of Dftn such that

C15c: ( plxpn2 = the Enumeration of places_of dct . (x + n2) & plxpn2 in rng dct ) ;

C16c: plxpn2 <> p2 by FUNCT_1:def 4, A39a, C18a, C21c, C15c, C22;

n1 + 0 < n2 + x by XREAL_1:8, S1;

then plxpn2 <> p1 by FUNCT_1:def 4, A39, C18, C21c, C15c;

then C14c: ( not plxpn2 in *' {t} & not plxpn2 in {t} *' ) by L4, C16c, C15c;

thus ( the Enumeration of M0, places_of dct /^ n2) . x = the Enumeration of M0, places_of dct . (x + n2) by RFINSEQ:def 1, A36, C13c

.= M0 . plxpn2 by K23, Def12, C15c, C10c

.= (Firing (t,M0)) . plxpn2 by Def11, C14c, A10

.= the Enumeration of Firing (t,M0), places_of dct . (x + n2) by K23, Def12, C10cc, C15c

.= ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . x by RFINSEQ:def 1, C13c, C1c, A36a ; :: thesis: verum

.= ((Sum (((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= (((Sum ((( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of M0, places_of dct /. n2)*>)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:75

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of M0, places_of dct /. n2)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) | (n1 -' 1))) + (( the Enumeration of M0, places_of dct | (n2 -' 1)) /. n1)) + (Sum (( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of M0, places_of dct /. n2)) + (Sum ( the Enumeration of M0, places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by A29, A29b, A29c, A29f

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + ( the Enumeration of Firing (t,M0), places_of dct /. n2)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:73

.= ((((Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1))) + (Sum <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:73

.= (((Sum ((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>)) + (Sum (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= ((Sum (((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1))) + (Sum <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= (Sum ((((( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) | (n1 -' 1)) ^ <*(( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /. n1)*>) ^ (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1)) ^ <*( the Enumeration of Firing (t,M0), places_of dct /. n2)*>)) + (Sum ( the Enumeration of Firing (t,M0), places_of dct /^ n2)) by RVSUM_1:75

.= num_marks ((places_of dct),(Firing (t,M0))) by RVSUM_1:75, A27a, G2 ; :: thesis: verum

proof

assume A59:
q .. the Enumeration of places_of dct = r .. the Enumeration of places_of dct
; :: thesis: contradiction

q = the Enumeration of places_of dct . (r .. the Enumeration of places_of dct) by A59, FINSEQ_4:19, A32a

.= r by FINSEQ_4:19, A32 ;

hence contradiction by A57; :: thesis: verum

end;q = the Enumeration of places_of dct . (r .. the Enumeration of places_of dct) by A59, FINSEQ_4:19, A32a

.= r by FINSEQ_4:19, A32 ;

hence contradiction by A57; :: thesis: verum

per cases then
( q .. the Enumeration of places_of dct > r .. the Enumeration of places_of dct or r .. the Enumeration of places_of dct > q .. the Enumeration of places_of dct )
by XXREAL_0:1;

end;

suppose
q .. the Enumeration of places_of dct > r .. the Enumeration of places_of dct
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

hence
num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))
by gen, A32, A32a, E1con, A30a, A30b; :: thesis: verum

end;suppose
r .. the Enumeration of places_of dct > q .. the Enumeration of places_of dct
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

hence
num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))
by gen, A32, A32a, E1cona, A30a, A30b; :: thesis: verum

end;suppose A9:
not t in transitions_of dct
; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))

set EF = the Enumeration of Firing (t,M0), places_of dct;

set E = the Enumeration of M0, places_of dct;

A15: len the Enumeration of Firing (t,M0), places_of dct = len the Enumeration of places_of dct by Def12, K23;

len the Enumeration of places_of dct = len the Enumeration of M0, places_of dct by Def12, K23;

then A4: dom the Enumeration of Firing (t,M0), places_of dct = dom the Enumeration of M0, places_of dct by FINSEQ_3:29, A15;

end;set E = the Enumeration of M0, places_of dct;

A15: len the Enumeration of Firing (t,M0), places_of dct = len the Enumeration of places_of dct by Def12, K23;

len the Enumeration of places_of dct = len the Enumeration of M0, places_of dct by Def12, K23;

then A4: dom the Enumeration of Firing (t,M0), places_of dct = dom the Enumeration of M0, places_of dct by FINSEQ_3:29, A15;

now :: thesis: for x being Element of NAT st x in dom the Enumeration of Firing (t,M0), places_of dct holds

the Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . x

hence
num_marks ((places_of dct),(Firing (t,M0))) = num_marks ((places_of dct),M0)
by PARTFUN1:5, A4; :: thesis: verumthe Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . x

let x be Element of NAT ; :: thesis: ( x in dom the Enumeration of Firing (t,M0), places_of dct implies the Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . x )

assume A6: x in dom the Enumeration of Firing (t,M0), places_of dct ; :: thesis: the Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . x

then x in dom the Enumeration of places_of dct by FINSEQ_3:29, A15;

then A18: the Enumeration of places_of dct . x in rng the Enumeration of places_of dct by FUNCT_1:3;

then reconsider s = the Enumeration of places_of dct . x as place of Dftn ;

A14: s in places_of dct by RLAFFIN3:def 1, A18;

.= M0 . ( the Enumeration of places_of dct . x) by A10, Def11, A7, P1

.= the Enumeration of M0, places_of dct . x by Def12, K23, A6, A4 ; :: thesis: verum

end;assume A6: x in dom the Enumeration of Firing (t,M0), places_of dct ; :: thesis: the Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . x

then x in dom the Enumeration of places_of dct by FINSEQ_3:29, A15;

then A18: the Enumeration of places_of dct . x in rng the Enumeration of places_of dct by FUNCT_1:3;

then reconsider s = the Enumeration of places_of dct . x as place of Dftn ;

A14: s in places_of dct by RLAFFIN3:def 1, A18;

A7: now :: thesis: ( s in *' {t} implies s in {t} *' )

assume
( s in *' {t} & not s in {t} *' )
; :: thesis: contradiction

then consider f being S-T_arc of Dftn, t1 being transition of Dftn such that

A13: ( t1 in {t} & f = [s,t1] ) by PETRI:6;

t1 = t by TARSKI:def 1, A13;

hence contradiction by A9, Thb, A14, A13; :: thesis: verum

end;then consider f being S-T_arc of Dftn, t1 being transition of Dftn such that

A13: ( t1 in {t} & f = [s,t1] ) by PETRI:6;

t1 = t by TARSKI:def 1, A13;

hence contradiction by A9, Thb, A14, A13; :: thesis: verum

P1: now :: thesis: ( s in {t} *' implies s in *' {t} )

thus the Enumeration of Firing (t,M0), places_of dct . x =
(Firing (t,M0)) . s
by Def12, K23, A6
assume
( s in {t} *' & not s in *' {t} )
; :: thesis: contradiction

then consider f being T-S_arc of Dftn, t1 being transition of Dftn such that

A13a: ( t1 in {t} & f = [t1,s] ) by PETRI:8;

t1 = t by TARSKI:def 1, A13a;

hence contradiction by A9, Thb, A14, A13a; :: thesis: verum

end;then consider f being T-S_arc of Dftn, t1 being transition of Dftn such that

A13a: ( t1 in {t} & f = [t1,s] ) by PETRI:8;

t1 = t by TARSKI:def 1, A13a;

hence contradiction by A9, Thb, A14, A13a; :: thesis: verum

.= M0 . ( the Enumeration of places_of dct . x) by A10, Def11, A7, P1

.= the Enumeration of M0, places_of dct . x by Def12, K23, A6, A4 ; :: thesis: verum