let Dftn be Decision_free_PT; 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; 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; 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; 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 )
;
suppose A10:
t is_firable_at M0
;
num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))per cases
( t in transitions_of dct or not t in transitions_of dct )
;
suppose
t in transitions_of dct
;
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;
per cases
( len dct = 3 or len dct > 3 )
by A21, XXREAL_0:1;
suppose K10:
len dct = 3
;
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)}
proof
thus
rng the
Enumeration of
places_of dct c= {(dct . 1)}
XBOOLE_0:def 10 {(dct . 1)} c= rng the Enumeration of places_of dctproof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(dct . 1)} or x in rng the Enumeration of places_of dct )
assume
x in {(dct . 1)}
;
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;
verum
end;
the
Enumeration of
places_of dct <> {}
by K21;
then X7:
len the
Enumeration of
places_of dct >= 0 + 1
by NAT_1:13;
A24:
len the
Enumeration of
places_of dct = 1
then A25:
len the
Enumeration of
Firing (
t,
M0),
places_of dct = 1
by Def12, K23;
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 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 . xlet x be
Element of
NAT ;
( 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
;
the Enumeration of M0, places_of dct . x = the Enumeration of Firing (t,M0), places_of dct . xthen
( 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
;
verum end; hence
num_marks (
(places_of dct),
(Firing (t,M0)))
= num_marks (
(places_of dct),
M0)
by PARTFUN1:5, K2;
verum end; suppose A74:
len dct > 3
;
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 A62:
1
< n
by A53a, XXREAL_0:1;
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
n < len dct
by A53, XXREAL_0:1;
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
;
contradiction
end; E1:
now 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} ) )let s be
place of
Dftn;
( 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
;
( ( 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} *' )
( s <> q implies not s in *' {t} )proof
assume D10:
(
s <> r &
s in {t} *' )
;
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;
per cases
( 1 = ns or ns = len dct or ( 1 < ns & ns < len dct ) )
by D2, XXREAL_0:1;
suppose A72:
( 1
= ns or
ns = len dct )
;
contradictionreconsider 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;
verum end; suppose D6:
( 1
< ns &
ns < len dct )
;
contradictionthen
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;
verum end;
end; thus
(
s <> q implies not
s in *' {t} )
verumproof
assume D10a:
(
s <> q &
s in *' {t} )
;
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;
per cases
( 1 = ns or ns = len dct or ( 1 < ns & ns < len dct ) )
by D2, XXREAL_0:1;
suppose A72b:
( 1
= ns or
ns = len dct )
;
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;
verum end; suppose D6:
( 1
< ns &
ns < len dct )
;
contradictionthen 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;
verum end;
end; end; E1con:
for
s being
place of
Dftn st
s in rng dct &
s <> q &
s <> r holds
( 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 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)))let n1,
n2 be
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)))let p1,
p2 be
place of
Dftn;
( 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 )
;
( 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} ) )
;
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
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
;
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;
suppose A29k:
(
p2 in *' {t} & not
p2 in {t} *' &
p1 in {t} *' & not
p1 in *' {t} )
;
(((( 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;
verum end; suppose A29l:
(
p1 in *' {t} & not
p1 in {t} *' &
p2 in {t} *' & not
p2 in *' {t} )
;
(((( 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;
verum end;
end; 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)
proof
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;
now 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)) . xlet x be
Element of
NAT ;
( 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))
;
(( 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)) . xthen 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
;
verum end;
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;
verum
end; A29b:
( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1 = ( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1
proof
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;
now 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) . xlet x be
Element of
NAT ;
( 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)
;
(( the Enumeration of M0, places_of dct | (n2 -' 1)) /^ n1) . x = (( the Enumeration of Firing (t,M0), places_of dct | (n2 -' 1)) /^ n1) . xthen 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
;
verum end;
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;
verum
end; A29c:
the
Enumeration of
M0,
places_of dct /^ n2 = the
Enumeration of
Firing (
t,
M0),
places_of dct /^ n2
proof
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;
now 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) . xlet x be
Element of
NAT ;
( 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)
;
( the Enumeration of M0, places_of dct /^ n2) . x = ( the Enumeration of Firing (t,M0), places_of dct /^ n2) . xthen 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
;
verum end;
hence
the
Enumeration of
M0,
places_of dct /^ n2 = the
Enumeration of
Firing (
t,
M0),
places_of dct /^ n2
by PARTFUN1:5, C1c;
verum
end; 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
.=
((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
;
verum end;
q .. the
Enumeration of
places_of dct <> r .. the
Enumeration of
places_of dct
end; end; suppose A9:
not
t in transitions_of dct
;
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;
now 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 . xlet x be
Element of
NAT ;
( 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
;
the Enumeration of Firing (t,M0), places_of dct . x = the Enumeration of M0, places_of dct . xthen
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;
thus the
Enumeration of
Firing (
t,
M0),
places_of dct . x =
(Firing (t,M0)) . s
by Def12, K23, A6
.=
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
;
verum end; hence
num_marks (
(places_of dct),
(Firing (t,M0)))
= num_marks (
(places_of dct),
M0)
by PARTFUN1:5, A4;
verum end;