deffunc H_{1}( Element of I) -> set = the carrier of (CPNT . $1);

consider P being ManySortedSet of I such that

AS1: for i being Element of I holds P . i = H_{1}(i)
from PBOOLE:sch 5();

deffunc H_{2}( Element of I) -> set = the carrier' of (CPNT . $1);

consider T being ManySortedSet of I such that

AS2: for i being Element of I holds T . i = H_{2}(i)
from PBOOLE:sch 5();

deffunc H_{3}( Element of I) -> Element of bool [: the carrier of (CPNT . $1), the carrier' of (CPNT . $1):] = the S-T_Arcs of (CPNT . $1);

consider ST being ManySortedSet of I such that

AS3: for i being Element of I holds ST . i = H_{3}(i)
from PBOOLE:sch 5();

deffunc H_{4}( Element of I) -> Element of bool [: the carrier' of (CPNT . $1), the carrier of (CPNT . $1):] = the T-S_Arcs of (CPNT . $1);

consider TS being ManySortedSet of I such that

AS4: for i being Element of I holds TS . i = H_{4}(i)
from PBOOLE:sch 5();

deffunc H_{5}( Element of I) -> set = the ColoredSet of (CPNT . $1);

consider CS being ManySortedSet of I such that

AS5: for i being Element of I holds CS . i = H_{5}(i)
from PBOOLE:sch 5();

deffunc H_{6}( Element of I) -> set = the firing-rule of (CPNT . $1);

consider F being ManySortedSet of I such that

AS6: for i being Element of I holds F . i = H_{6}(i)
from PBOOLE:sch 5();

deffunc H_{7}( Element of I) -> set = dom the firing-rule of (CPNT . $1);

consider DM being ManySortedSet of I such that

DM1: for i being Element of I holds DM . i = H_{7}(i)
from PBOOLE:sch 5();

deffunc H_{8}( Element of I) -> set = rng the firing-rule of (CPNT . $1);

consider RG being ManySortedSet of I such that

RG1: for i being Element of I holds RG . i = H_{8}(i)
from PBOOLE:sch 5();

set i = the Element of I;

P . the Element of I = the carrier of (CPNT . the Element of I) by AS1;

then consider x being object such that

S1: x in P . the Element of I by XBOOLE_0:def 1;

reconsider P0 = union (rng P) as non empty set by S1, TARSKI:def 4;

set i = the Element of I;

T . the Element of I = the carrier' of (CPNT . the Element of I) by AS2;

then consider x being object such that

S2: x in T . the Element of I by XBOOLE_0:def 1;

reconsider T0 = union (rng T) as non empty set by S2, TARSKI:def 4;

s: for X being set st X in rng ST holds

X c= [:P0,T0:]

ST . the Element of I = the S-T_Arcs of (CPNT . the Element of I) by AS3;

then consider x being object such that

S1: x in ST . the Element of I by XBOOLE_0:def 1;

reconsider ST0 = union (rng ST) as non empty Relation of P0,T0 by S1, TARSKI:def 4, s, ZFMISC_1:76;

for X being set st X in rng TS holds

X c= [:T0,P0:]

for X being set st X in rng O holds

X c= [:T0,P0:]

set i = the Element of I;

TS . the Element of I = the T-S_Arcs of (CPNT . the Element of I) by AS4;

then consider x being object such that

S1: x in TS . the Element of I by XBOOLE_0:def 1;

x in union (rng TS) by S1, TARSKI:def 4;

then reconsider TS0 = (union (rng TS)) \/ (union (rng O)) as non empty Relation of T0,P0 by t, PTS0, XBOOLE_1:8;

LL0: for X being set st X in rng CS holds

X is finite

set i = the Element of I;

CS . the Element of I = the ColoredSet of (CPNT . the Element of I) by AS5;

then consider x being object such that

S5: x in CS . the Element of I by XBOOLE_0:def 1;

reconsider CS0 = union (rng CS) as non empty finite set by S5, TARSKI:def 4, LL0, ll3, FINSET_1:7, FINSET_1:8;

LL41: for i being object st i in I holds

ex f being Function st

( f = F . i & dom f = DM . i & rng f = RG . i )

for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds

dom f misses dom g

LL43: ( F0 = union (rng F) & dom F0 = union (rng DM) & rng F0 = union (rng RG) & ( for i, x being object

for f being Function st i in I & f = F . i & x in dom f holds

F0 . x = f . x ) ) by LM01, LL41;

reconsider UQ = union (rng q) as Function by LMQ1, AS;

set UF0 = F0 +* UQ;

reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored_Petri_net by PETRI:def 1, PETRI:def 2;

deffunc H_{9}( Element of I) -> Element of bool the carrier' of (CPNT . $1) = Outbds (CPNT . $1);

consider OU being Function such that

OU1: ( dom OU = I & ( for i being Element of I holds OU . i = H_{9}(i) ) )
from FUNCT_1:sch 4();

reconsider OU = OU as I -defined Function by OU1, RELAT_1:def 18;

reconsider OU = OU as ManySortedSet of I by OU1, PARTFUN1:def 2;

for x0 being object st x0 in Outbds SCPNT holds

x0 in union (rng OU)

XX3: for i, j being object st i in I & j in I & i <> j holds

(T . i) /\ (OU . j) = {}

DM . i c= (T (\) OU) . i

then XXX3A: dom F0 c= the carrier' of SCPNT \ (Union OU) by LL43, v, LM04, XX3, PBOOLE:def 2;

xx: the carrier' of SCPNT \ (union (rng OU)) c= the carrier' of SCPNT \ (Outbds SCPNT) by OU2, XBOOLE_1:34;

for x being object st x in dom the firing-rule of SCPNT holds

x in the carrier' of SCPNT \ (Outbds SCPNT)

for t being transition of SCPNT st t in dom the firing-rule of SCPNT holds

ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

take SCPNT ; :: thesis: ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ )

thus ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ ) by AS1, AS2, AS3, AS4, AS5, AS6, LL43; :: thesis: verum

consider P being ManySortedSet of I such that

AS1: for i being Element of I holds P . i = H

deffunc H

consider T being ManySortedSet of I such that

AS2: for i being Element of I holds T . i = H

deffunc H

consider ST being ManySortedSet of I such that

AS3: for i being Element of I holds ST . i = H

deffunc H

consider TS being ManySortedSet of I such that

AS4: for i being Element of I holds TS . i = H

deffunc H

consider CS being ManySortedSet of I such that

AS5: for i being Element of I holds CS . i = H

deffunc H

consider F being ManySortedSet of I such that

AS6: for i being Element of I holds F . i = H

deffunc H

consider DM being ManySortedSet of I such that

DM1: for i being Element of I holds DM . i = H

deffunc H

consider RG being ManySortedSet of I such that

RG1: for i being Element of I holds RG . i = H

set i = the Element of I;

P . the Element of I = the carrier of (CPNT . the Element of I) by AS1;

then consider x being object such that

S1: x in P . the Element of I by XBOOLE_0:def 1;

reconsider P0 = union (rng P) as non empty set by S1, TARSKI:def 4;

set i = the Element of I;

T . the Element of I = the carrier' of (CPNT . the Element of I) by AS2;

then consider x being object such that

S2: x in T . the Element of I by XBOOLE_0:def 1;

reconsider T0 = union (rng T) as non empty set by S2, TARSKI:def 4;

s: for X being set st X in rng ST holds

X c= [:P0,T0:]

proof

set i = the Element of I;
let X be set ; :: thesis: ( X in rng ST implies X c= [:P0,T0:] )

assume X in rng ST ; :: thesis: X c= [:P0,T0:]

then consider i being object such that

L1: ( i in dom ST & X = ST . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by L1;

l2: X = the S-T_Arcs of (CPNT . i) by L1, AS3;

l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . i c= P0 by ZFMISC_1:74;

then [:(P . i),(T . i):] c= [:P0,T0:] by L4, ZFMISC_1:96;

hence X c= [:P0,T0:] by l3, l2; :: thesis: verum

end;assume X in rng ST ; :: thesis: X c= [:P0,T0:]

then consider i being object such that

L1: ( i in dom ST & X = ST . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by L1;

l2: X = the S-T_Arcs of (CPNT . i) by L1, AS3;

l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . i c= P0 by ZFMISC_1:74;

then [:(P . i),(T . i):] c= [:P0,T0:] by L4, ZFMISC_1:96;

hence X c= [:P0,T0:] by l3, l2; :: thesis: verum

ST . the Element of I = the S-T_Arcs of (CPNT . the Element of I) by AS3;

then consider x being object such that

S1: x in ST . the Element of I by XBOOLE_0:def 1;

reconsider ST0 = union (rng ST) as non empty Relation of P0,T0 by S1, TARSKI:def 4, s, ZFMISC_1:76;

for X being set st X in rng TS holds

X c= [:T0,P0:]

proof

then PTS0:
union (rng TS) c= [:T0,P0:]
by ZFMISC_1:76;
let X be set ; :: thesis: ( X in rng TS implies X c= [:T0,P0:] )

assume X in rng TS ; :: thesis: X c= [:T0,P0:]

then consider i being object such that

L1: ( i in dom TS & X = TS . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by L1;

l2: X = the T-S_Arcs of (CPNT . i) by L1, AS4;

l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . i c= P0 by ZFMISC_1:74;

then [:(T . i),(P . i):] c= [:T0,P0:] by L4, ZFMISC_1:96;

hence X c= [:T0,P0:] by l3, l2; :: thesis: verum

end;assume X in rng TS ; :: thesis: X c= [:T0,P0:]

then consider i being object such that

L1: ( i in dom TS & X = TS . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by L1;

l2: X = the T-S_Arcs of (CPNT . i) by L1, AS4;

l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . i c= P0 by ZFMISC_1:74;

then [:(T . i),(P . i):] c= [:T0,P0:] by L4, ZFMISC_1:96;

hence X c= [:T0,P0:] by l3, l2; :: thesis: verum

for X being set st X in rng O holds

X c= [:T0,P0:]

proof

then t:
union (rng O) c= [:T0,P0:]
by ZFMISC_1:76;
let X be set ; :: thesis: ( X in rng O implies X c= [:T0,P0:] )

assume X in rng O ; :: thesis: X c= [:T0,P0:]

then consider z being object such that

L1: ( z in dom O & X = O . z ) by FUNCT_1:def 3;

z in XorDelta I by L1;

then consider i, j being Element of I such that

L11: ( z = [i,j] & i <> j ) ;

l12: O . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by L11, Defcntmap;

L14: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . j c= P0 by ZFMISC_1:74;

then L13: [:(T . i),(P . j):] c= [:T0,P0:] by L4, ZFMISC_1:96;

[:(Outbds (CPNT . i)), the carrier of (CPNT . j):] c= [:(T . i),(P . j):] by L14, ZFMISC_1:96;

hence X c= [:T0,P0:] by L13, l12, L11, L1; :: thesis: verum

end;assume X in rng O ; :: thesis: X c= [:T0,P0:]

then consider z being object such that

L1: ( z in dom O & X = O . z ) by FUNCT_1:def 3;

z in XorDelta I by L1;

then consider i, j being Element of I such that

L11: ( z = [i,j] & i <> j ) ;

l12: O . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by L11, Defcntmap;

L14: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by AS1, AS2;

L4: T . i c= T0 by ZFMISC_1:74;

P . j c= P0 by ZFMISC_1:74;

then L13: [:(T . i),(P . j):] c= [:T0,P0:] by L4, ZFMISC_1:96;

[:(Outbds (CPNT . i)), the carrier of (CPNT . j):] c= [:(T . i),(P . j):] by L14, ZFMISC_1:96;

hence X c= [:T0,P0:] by L13, l12, L11, L1; :: thesis: verum

set i = the Element of I;

TS . the Element of I = the T-S_Arcs of (CPNT . the Element of I) by AS4;

then consider x being object such that

S1: x in TS . the Element of I by XBOOLE_0:def 1;

x in union (rng TS) by S1, TARSKI:def 4;

then reconsider TS0 = (union (rng TS)) \/ (union (rng O)) as non empty Relation of T0,P0 by t, PTS0, XBOOLE_1:8;

LL0: for X being set st X in rng CS holds

X is finite

proof

ll3:
dom CS is finite
;
let X be set ; :: thesis: ( X in rng CS implies X is finite )

assume X in rng CS ; :: thesis: X is finite

then consider i being object such that

LL1: ( i in dom CS & X = CS . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by LL1;

X = the ColoredSet of (CPNT . i) by LL1, AS5;

hence X is finite ; :: thesis: verum

end;assume X in rng CS ; :: thesis: X is finite

then consider i being object such that

LL1: ( i in dom CS & X = CS . i ) by FUNCT_1:def 3;

reconsider i = i as Element of I by LL1;

X = the ColoredSet of (CPNT . i) by LL1, AS5;

hence X is finite ; :: thesis: verum

set i = the Element of I;

CS . the Element of I = the ColoredSet of (CPNT . the Element of I) by AS5;

then consider x being object such that

S5: x in CS . the Element of I by XBOOLE_0:def 1;

reconsider CS0 = union (rng CS) as non empty finite set by S5, TARSKI:def 4, LL0, ll3, FINSET_1:7, FINSET_1:8;

LL41: for i being object st i in I holds

ex f being Function st

( f = F . i & dom f = DM . i & rng f = RG . i )

proof

for i, j being object
let i be object ; :: thesis: ( i in I implies ex f being Function st

( f = F . i & dom f = DM . i & rng f = RG . i ) )

assume i in I ; :: thesis: ex f being Function st

( f = F . i & dom f = DM . i & rng f = RG . i )

then reconsider i0 = i as Element of I ;

P04: F . i0 = the firing-rule of (CPNT . i0) by AS6;

then reconsider f = F . i as Function ;

take f ; :: thesis: ( f = F . i & dom f = DM . i & rng f = RG . i )

thus f = F . i ; :: thesis: ( dom f = DM . i & rng f = RG . i )

thus dom f = DM . i by P04, DM1; :: thesis: rng f = RG . i

thus rng f = RG . i by P04, RG1; :: thesis: verum

end;( f = F . i & dom f = DM . i & rng f = RG . i ) )

assume i in I ; :: thesis: ex f being Function st

( f = F . i & dom f = DM . i & rng f = RG . i )

then reconsider i0 = i as Element of I ;

P04: F . i0 = the firing-rule of (CPNT . i0) by AS6;

then reconsider f = F . i as Function ;

take f ; :: thesis: ( f = F . i & dom f = DM . i & rng f = RG . i )

thus f = F . i ; :: thesis: ( dom f = DM . i & rng f = RG . i )

thus dom f = DM . i by P04, DM1; :: thesis: rng f = RG . i

thus rng f = RG . i by P04, RG1; :: thesis: verum

for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds

dom f misses dom g

proof

then consider F0 being Function such that
let i0, j0 be object ; :: thesis: for f, g being Function st i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 holds

dom f misses dom g

let f, g be Function; :: thesis: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 implies dom f misses dom g )

assume AA1: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 ) ; :: thesis: dom f misses dom g

then reconsider i = i0, j = j0 as Element of I ;

AA4: dom f = dom the firing-rule of (CPNT . i) by AA1, AS6;

AA5: dom g = dom the firing-rule of (CPNT . j) by AA1, AS6;

AA6: ( dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) & dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) ) by PETRI_2:def 11;

thus dom f misses dom g :: thesis: verum

end;dom f misses dom g

let f, g be Function; :: thesis: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 implies dom f misses dom g )

assume AA1: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 ) ; :: thesis: dom f misses dom g

then reconsider i = i0, j = j0 as Element of I ;

AA4: dom f = dom the firing-rule of (CPNT . i) by AA1, AS6;

AA5: dom g = dom the firing-rule of (CPNT . j) by AA1, AS6;

AA6: ( dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) & dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) ) by PETRI_2:def 11;

thus dom f misses dom g :: thesis: verum

proof

assume
not dom f misses dom g
; :: thesis: contradiction

then (dom f) /\ (dom g) <> {} by XBOOLE_0:def 7;

then consider x being object such that

AA8: x in (dom f) /\ (dom g) by XBOOLE_0:def 1;

x in dom f by AA8, XBOOLE_0:def 4;

then a9: x in the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by AA4, AA6;

x in dom g by XBOOLE_0:def 4, AA8;

then x in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by AA5, AA6;

then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by a9, XBOOLE_0:def 4;

hence contradiction by AS, AA1, XBOOLE_0:def 7; :: thesis: verum

end;then (dom f) /\ (dom g) <> {} by XBOOLE_0:def 7;

then consider x being object such that

AA8: x in (dom f) /\ (dom g) by XBOOLE_0:def 1;

x in dom f by AA8, XBOOLE_0:def 4;

then a9: x in the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by AA4, AA6;

x in dom g by XBOOLE_0:def 4, AA8;

then x in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by AA5, AA6;

then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by a9, XBOOLE_0:def 4;

hence contradiction by AS, AA1, XBOOLE_0:def 7; :: thesis: verum

LL43: ( F0 = union (rng F) & dom F0 = union (rng DM) & rng F0 = union (rng RG) & ( for i, x being object

for f being Function st i in I & f = F . i & x in dom f holds

F0 . x = f . x ) ) by LM01, LL41;

reconsider UQ = union (rng q) as Function by LMQ1, AS;

set UF0 = F0 +* UQ;

reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored_Petri_net by PETRI:def 1, PETRI:def 2;

deffunc H

consider OU being Function such that

OU1: ( dom OU = I & ( for i being Element of I holds OU . i = H

reconsider OU = OU as I -defined Function by OU1, RELAT_1:def 18;

reconsider OU = OU as ManySortedSet of I by OU1, PARTFUN1:def 2;

for x0 being object st x0 in Outbds SCPNT holds

x0 in union (rng OU)

proof

then OU2:
Outbds SCPNT c= union (rng OU)
;
let x0 be object ; :: thesis: ( x0 in Outbds SCPNT implies x0 in union (rng OU) )

assume x0 in Outbds SCPNT ; :: thesis: x0 in union (rng OU)

then consider x1 being transition of SCPNT such that

OU2: ( x0 = x1 & x1 is outbound ) ;

consider Z being set such that

OU3: ( x1 in Z & Z in rng T ) by TARSKI:def 4;

consider i being object such that

OU4: ( i in dom T & Z = T . i ) by OU3, FUNCT_1:def 3;

reconsider i = i as Element of I by OU4;

reconsider xi = x1 as transitions of (CPNT . i) by AS2, OU3, OU4;

{xi} *' = {}

then OU6: xi in Outbds (CPNT . i) ;

OU . i = Outbds (CPNT . i) by OU1;

hence x0 in union (rng OU) by OU2, OU6, TARSKI:def 4; :: thesis: verum

end;assume x0 in Outbds SCPNT ; :: thesis: x0 in union (rng OU)

then consider x1 being transition of SCPNT such that

OU2: ( x0 = x1 & x1 is outbound ) ;

consider Z being set such that

OU3: ( x1 in Z & Z in rng T ) by TARSKI:def 4;

consider i being object such that

OU4: ( i in dom T & Z = T . i ) by OU3, FUNCT_1:def 3;

reconsider i = i as Element of I by OU4;

reconsider xi = x1 as transitions of (CPNT . i) by AS2, OU3, OU4;

{xi} *' = {}

proof

then
xi is outbound
;
assume
{xi} *' <> {}
; :: thesis: contradiction

then consider z being object such that

OU61: z in {xi} *' by XBOOLE_0:def 1;

consider si being place of (CPNT . i) such that

OU62: ( z = si & ex fi being T-S_arc of (CPNT . i) ex ti being transition of (CPNT . i) st

( ti in {xi} & fi = [ti,si] ) ) by OU61;

consider fi being T-S_arc of (CPNT . i), ti being transition of (CPNT . i) such that

OU63: ( ti in {xi} & fi = [ti,si] ) by OU62;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = si as place of SCPNT by SS0, TARSKI:def 4;

TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;

fi in union (rng TS) by TS0, TARSKI:def 4;

then reconsider ff = fi as T-S_arc of SCPNT by XBOOLE_0:def 3;

TT0: T . i = the carrier' of (CPNT . i) by AS2;

reconsider tt = ti as transition of SCPNT by TT0, TARSKI:def 4;

ff = [tt,ss] by OU63;

then ss in { s where s is place of SCPNT : ex f being T-S_arc of SCPNT ex t being transition of SCPNT st

( t in {x1} & f = [t,s] ) } by OU63;

hence contradiction by OU2; :: thesis: verum

end;then consider z being object such that

OU61: z in {xi} *' by XBOOLE_0:def 1;

consider si being place of (CPNT . i) such that

OU62: ( z = si & ex fi being T-S_arc of (CPNT . i) ex ti being transition of (CPNT . i) st

( ti in {xi} & fi = [ti,si] ) ) by OU61;

consider fi being T-S_arc of (CPNT . i), ti being transition of (CPNT . i) such that

OU63: ( ti in {xi} & fi = [ti,si] ) by OU62;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = si as place of SCPNT by SS0, TARSKI:def 4;

TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;

fi in union (rng TS) by TS0, TARSKI:def 4;

then reconsider ff = fi as T-S_arc of SCPNT by XBOOLE_0:def 3;

TT0: T . i = the carrier' of (CPNT . i) by AS2;

reconsider tt = ti as transition of SCPNT by TT0, TARSKI:def 4;

ff = [tt,ss] by OU63;

then ss in { s where s is place of SCPNT : ex f being T-S_arc of SCPNT ex t being transition of SCPNT st

( t in {x1} & f = [t,s] ) } by OU63;

hence contradiction by OU2; :: thesis: verum

then OU6: xi in Outbds (CPNT . i) ;

OU . i = Outbds (CPNT . i) by OU1;

hence x0 in union (rng OU) by OU2, OU6, TARSKI:def 4; :: thesis: verum

XX3: for i, j being object st i in I & j in I & i <> j holds

(T . i) /\ (OU . j) = {}

proof

v:
for i being object st i in I holds
let i0, j0 be object ; :: thesis: ( i0 in I & j0 in I & i0 <> j0 implies (T . i0) /\ (OU . j0) = {} )

assume XXX: ( i0 in I & j0 in I & i0 <> j0 ) ; :: thesis: (T . i0) /\ (OU . j0) = {}

then reconsider i = i0, j = j0 as Element of I ;

P1: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) by XBOOLE_1:26;

p2: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= {} by P1, XBOOLE_0:def 7, AS, XXX;

the carrier' of (CPNT . i) = T . i by AS2;

hence (T . i0) /\ (OU . j0) = {} by p2, OU1; :: thesis: verum

end;assume XXX: ( i0 in I & j0 in I & i0 <> j0 ) ; :: thesis: (T . i0) /\ (OU . j0) = {}

then reconsider i = i0, j = j0 as Element of I ;

P1: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) by XBOOLE_1:26;

p2: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= {} by P1, XBOOLE_0:def 7, AS, XXX;

the carrier' of (CPNT . i) = T . i by AS2;

hence (T . i0) /\ (OU . j0) = {} by p2, OU1; :: thesis: verum

DM . i c= (T (\) OU) . i

proof

XXX2:
( union (rng DM) = Union DM & union (rng T) = Union T & union (rng OU) = Union OU )
by CARD_3:def 4;
let i0 be object ; :: thesis: ( i0 in I implies DM . i0 c= (T (\) OU) . i0 )

assume i0 in I ; :: thesis: DM . i0 c= (T (\) OU) . i0

then reconsider i = i0 as Element of I ;

P1: DM . i = dom the firing-rule of (CPNT . i) by DM1;

P2: dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by PETRI_2:def 11;

P3: the carrier' of (CPNT . i) = T . i by AS2;

(T (\) OU) . i = (T . i) \ (OU . i) by PBOOLE:def 6;

hence DM . i0 c= (T (\) OU) . i0 by P1, P2, P3, OU1; :: thesis: verum

end;assume i0 in I ; :: thesis: DM . i0 c= (T (\) OU) . i0

then reconsider i = i0 as Element of I ;

P1: DM . i = dom the firing-rule of (CPNT . i) by DM1;

P2: dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by PETRI_2:def 11;

P3: the carrier' of (CPNT . i) = T . i by AS2;

(T (\) OU) . i = (T . i) \ (OU . i) by PBOOLE:def 6;

hence DM . i0 c= (T (\) OU) . i0 by P1, P2, P3, OU1; :: thesis: verum

then XXX3A: dom F0 c= the carrier' of SCPNT \ (Union OU) by LL43, v, LM04, XX3, PBOOLE:def 2;

xx: the carrier' of SCPNT \ (union (rng OU)) c= the carrier' of SCPNT \ (Outbds SCPNT) by OU2, XBOOLE_1:34;

for x being object st x in dom the firing-rule of SCPNT holds

x in the carrier' of SCPNT \ (Outbds SCPNT)

proof

then CP1:
dom the firing-rule of SCPNT c= the carrier' of SCPNT \ (Outbds SCPNT)
;
let x be object ; :: thesis: ( x in dom the firing-rule of SCPNT implies x in the carrier' of SCPNT \ (Outbds SCPNT) )

assume x in dom the firing-rule of SCPNT ; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)

end;assume x in dom the firing-rule of SCPNT ; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)

per cases then
( x in dom F0 or x in dom UQ )
by FUNCT_4:12;

end;

suppose AG1:
x in dom UQ
; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)

consider s being object such that

D2: [x,s] in UQ by AG1, XTUPLE_0:def 12;

consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

D3: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [x,s] in q12 ) by LMQ1, AS, D2;

CT1: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by AS1, AS2;

x in dom q12 by D3, XTUPLE_0:def 12;

then S0: x in Outbds (CPNT . i) by D3, FUNCT_2:92;

w: T . i c= T0 by ZFMISC_1:74;

then S2: x in the carrier' of SCPNT by S0, CT1;

reconsider t = x as transition of SCPNT by w, S0, CT1;

t in dom O12 by S0, FUNCT_2:def 1;

then consider s being object such that

A65: [t,s] in O12 by XTUPLE_0:def 12;

[i,j] in XorDelta I by D3;

then [i,j] in dom O by PARTFUN1:def 2;

then O . [i,j] in rng O by FUNCT_1:3;

then [t,s] in union (rng O) by D3, A65, TARSKI:def 4;

then reconsider f = [t,s] as T-S_arc of SCPNT by XBOOLE_0:def 3;

A68: f = [t,s] ;

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

U2: s in the carrier of (CPNT . j) by A65, ZFMISC_1:87;

P . j c= P0 by ZFMISC_1:74;

then s in {t} *' by A69, A68, U2, CT1;

then for w being transition of SCPNT holds

( not t = w or not w is outbound ) ;

then not x in Outbds SCPNT ;

hence x in the carrier' of SCPNT \ (Outbds SCPNT) by S2, XBOOLE_0:def 5; :: thesis: verum

end;D2: [x,s] in UQ by AG1, XTUPLE_0:def 12;

consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

D3: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [x,s] in q12 ) by LMQ1, AS, D2;

CT1: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by AS1, AS2;

x in dom q12 by D3, XTUPLE_0:def 12;

then S0: x in Outbds (CPNT . i) by D3, FUNCT_2:92;

w: T . i c= T0 by ZFMISC_1:74;

then S2: x in the carrier' of SCPNT by S0, CT1;

reconsider t = x as transition of SCPNT by w, S0, CT1;

t in dom O12 by S0, FUNCT_2:def 1;

then consider s being object such that

A65: [t,s] in O12 by XTUPLE_0:def 12;

[i,j] in XorDelta I by D3;

then [i,j] in dom O by PARTFUN1:def 2;

then O . [i,j] in rng O by FUNCT_1:3;

then [t,s] in union (rng O) by D3, A65, TARSKI:def 4;

then reconsider f = [t,s] as T-S_arc of SCPNT by XBOOLE_0:def 3;

A68: f = [t,s] ;

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

U2: s in the carrier of (CPNT . j) by A65, ZFMISC_1:87;

P . j c= P0 by ZFMISC_1:74;

then s in {t} *' by A69, A68, U2, CT1;

then for w being transition of SCPNT holds

( not t = w or not w is outbound ) ;

then not x in Outbds SCPNT ;

hence x in the carrier' of SCPNT \ (Outbds SCPNT) by S2, XBOOLE_0:def 5; :: thesis: verum

for t being transition of SCPNT st t in dom the firing-rule of SCPNT holds

ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

proof

then reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored-PT-net by PETRI_2:def 11, CP1;
let t be transition of SCPNT; :: thesis: ( t in dom the firing-rule of SCPNT implies ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) )

assume d: t in dom the firing-rule of SCPNT ; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

end;assume d: t in dom the firing-rule of SCPNT ; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

per cases
( not t in dom UQ or t in dom UQ )
;

end;

suppose AG01:
not t in dom UQ
; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

then AG0:
t in dom F0
by d, FUNCT_4:12;

consider Z being set such that

XOU3: ( t in Z & Z in rng T ) by TARSKI:def 4;

consider i being object such that

XOU4: ( i in dom T & Z = T . i ) by XOU3, FUNCT_1:def 3;

reconsider i = i as Element of I by XOU4;

reconsider ti = t as transitions of (CPNT . i) by XOU3, XOU4, AS2;

consider Z being set such that

POU3: ( t in Z & Z in rng DM ) by LL43, AG0, TARSKI:def 4;

consider j being object such that

POU4: ( j in dom DM & Z = DM . j ) by POU3, FUNCT_1:def 3;

reconsider j = j as Element of I by POU4;

OU6: DM . j = dom the firing-rule of (CPNT . j) by DM1;

i = j

consider CSi being non empty Subset of the ColoredSet of (CPNT . i), Ii being Subset of (*' {ti}), Oi being Subset of ({ti} *') such that

OU9: the firing-rule of (CPNT . i) . ti is Function of (thin_cylinders (CSi,Ii)),(thin_cylinders (CSi,Oi)) by PETRI_2:def 11, OU8;

CC1: CS . i c= union (rng CS) by ZFMISC_1:74;

CS . i = the ColoredSet of (CPNT . i) by AS5;

then reconsider CS = CSi as non empty Subset of the ColoredSet of SCPNT by CC1, XBOOLE_1:1;

Ii c= *' {t}

Oi c= {t} *'

Y1: F . i = the firing-rule of (CPNT . i) by AS6;

the firing-rule of SCPNT . t = F0 . t by AG01, FUNCT_4:11

.= the firing-rule of (CPNT . i) . ti by Y1, OU8, LL43 ;

then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I0)),(thin_cylinders (CS,O)) by OU9;

hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum

end;consider Z being set such that

XOU3: ( t in Z & Z in rng T ) by TARSKI:def 4;

consider i being object such that

XOU4: ( i in dom T & Z = T . i ) by XOU3, FUNCT_1:def 3;

reconsider i = i as Element of I by XOU4;

reconsider ti = t as transitions of (CPNT . i) by XOU3, XOU4, AS2;

consider Z being set such that

POU3: ( t in Z & Z in rng DM ) by LL43, AG0, TARSKI:def 4;

consider j being object such that

POU4: ( j in dom DM & Z = DM . j ) by POU3, FUNCT_1:def 3;

reconsider j = j as Element of I by POU4;

OU6: DM . j = dom the firing-rule of (CPNT . j) by DM1;

i = j

proof

then OU8:
ti in dom the firing-rule of (CPNT . i)
by POU3, POU4, DM1;
assume OU71:
i <> j
; :: thesis: contradiction

OU72: t in the carrier' of (CPNT . i) by XOU3, XOU4, AS2;

dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by PETRI_2:def 11;

then t in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by POU3, POU4, OU6;

then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by OU72, XBOOLE_0:def 4;

hence contradiction by AS, OU71, XBOOLE_0:def 7; :: thesis: verum

end;OU72: t in the carrier' of (CPNT . i) by XOU3, XOU4, AS2;

dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by PETRI_2:def 11;

then t in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by POU3, POU4, OU6;

then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by OU72, XBOOLE_0:def 4;

hence contradiction by AS, OU71, XBOOLE_0:def 7; :: thesis: verum

consider CSi being non empty Subset of the ColoredSet of (CPNT . i), Ii being Subset of (*' {ti}), Oi being Subset of ({ti} *') such that

OU9: the firing-rule of (CPNT . i) . ti is Function of (thin_cylinders (CSi,Ii)),(thin_cylinders (CSi,Oi)) by PETRI_2:def 11, OU8;

CC1: CS . i c= union (rng CS) by ZFMISC_1:74;

CS . i = the ColoredSet of (CPNT . i) by AS5;

then reconsider CS = CSi as non empty Subset of the ColoredSet of SCPNT by CC1, XBOOLE_1:1;

Ii c= *' {t}

proof

then reconsider I0 = Ii as Subset of (*' {t}) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ii or x in *' {t} )

assume x in Ii ; :: thesis: x in *' {t}

then x in *' {ti} ;

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [ssi,tti] ) ) ;

consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;

reconsider ff = ffi as S-T_arc of SCPNT by ST0, TARSKI:def 4;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [ss,tt] by XX2;

hence x in *' {t} by XX1, XX2; :: thesis: verum

end;assume x in Ii ; :: thesis: x in *' {t}

then x in *' {ti} ;

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [ssi,tti] ) ) ;

consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;

reconsider ff = ffi as S-T_arc of SCPNT by ST0, TARSKI:def 4;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [ss,tt] by XX2;

hence x in *' {t} by XX1, XX2; :: thesis: verum

Oi c= {t} *'

proof

then reconsider O = Oi as Subset of ({t} *') ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Oi or x in {t} *' )

assume x in Oi ; :: thesis: x in {t} *'

then x in {ti} *' ;

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being T-S_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [tti,ssi] ) ) ;

consider ffi being T-S_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [tti,ssi] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;

ffi in union (rng TS) by TS0, TARSKI:def 4;

then reconsider ff = ffi as T-S_arc of SCPNT by XBOOLE_0:def 3;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [tt,ss] by XX2;

hence x in {t} *' by XX1, XX2; :: thesis: verum

end;assume x in Oi ; :: thesis: x in {t} *'

then x in {ti} *' ;

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being T-S_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [tti,ssi] ) ) ;

consider ffi being T-S_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [tti,ssi] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;

ffi in union (rng TS) by TS0, TARSKI:def 4;

then reconsider ff = ffi as T-S_arc of SCPNT by XBOOLE_0:def 3;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [tt,ss] by XX2;

hence x in {t} *' by XX1, XX2; :: thesis: verum

Y1: F . i = the firing-rule of (CPNT . i) by AS6;

the firing-rule of SCPNT . t = F0 . t by AG01, FUNCT_4:11

.= the firing-rule of (CPNT . i) . ti by Y1, OU8, LL43 ;

then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I0)),(thin_cylinders (CS,O)) by OU9;

hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum

suppose AG1:
t in dom UQ
; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))

then consider s being object such that

D2: [t,s] in UQ by XTUPLE_0:def 12;

consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

D3: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [t,s] in q12 ) by LMQ1, AS, D2;

CT1: the ColoredSet of (CPNT . i) = CS . i by AS5;

DF1: t in dom q12 by D3, XTUPLE_0:def 12;

then S0: t in Outbds (CPNT . i) by D3, FUNCT_2:92;

then reconsider ti = t as transition of (CPNT . i) ;

v8: ex x being transition of (CPNT . i) st

( ti = x & x is outbound ) by S0;

CS . i = the ColoredSet of (CPNT . i) by AS5;

then reconsider CS0 = CS . i as non empty Subset of the ColoredSet of SCPNT by ZFMISC_1:74;

*' {ti} c= *' {t}

Im (O12,ti) c= {t} *'

the firing-rule of SCPNT . t = UQ . t by AG1, FUNCT_4:13

.= q12 . ti by DF1, D3, LMQ1A ;

then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS0,I0)),(thin_cylinders (CS0,O0)) by v8, CT1, D3;

hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum

end;D2: [t,s] in UQ by XTUPLE_0:def 12;

consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

D3: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [t,s] in q12 ) by LMQ1, AS, D2;

CT1: the ColoredSet of (CPNT . i) = CS . i by AS5;

DF1: t in dom q12 by D3, XTUPLE_0:def 12;

then S0: t in Outbds (CPNT . i) by D3, FUNCT_2:92;

then reconsider ti = t as transition of (CPNT . i) ;

v8: ex x being transition of (CPNT . i) st

( ti = x & x is outbound ) by S0;

CS . i = the ColoredSet of (CPNT . i) by AS5;

then reconsider CS0 = CS . i as non empty Subset of the ColoredSet of SCPNT by ZFMISC_1:74;

*' {ti} c= *' {t}

proof

then reconsider I0 = *' {ti} as Subset of (*' {t}) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in *' {ti} or x in *' {t} )

assume x in *' {ti} ; :: thesis: x in *' {t}

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [ssi,tti] ) ) ;

consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;

reconsider ff = ffi as S-T_arc of SCPNT by ST0, TARSKI:def 4;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [ss,tt] by XX2;

hence x in *' {t} by XX1, XX2; :: thesis: verum

end;assume x in *' {ti} ; :: thesis: x in *' {t}

then consider ssi being place of (CPNT . i) such that

XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st

( tti in {ti} & ffi = [ssi,tti] ) ) ;

consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that

XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;

SS0: P . i = the carrier of (CPNT . i) by AS1;

reconsider ss = ssi as place of SCPNT by SS0, TARSKI:def 4;

ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;

reconsider ff = ffi as S-T_arc of SCPNT by ST0, TARSKI:def 4;

tti = t by XX2, TARSKI:def 1;

then reconsider tt = tti as transition of SCPNT ;

ff = [ss,tt] by XX2;

hence x in *' {t} by XX1, XX2; :: thesis: verum

Im (O12,ti) c= {t} *'

proof

then reconsider O0 = Im (O12,ti) as Subset of ({t} *') ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Im (O12,ti) or x in {t} *' )

assume A41: x in Im (O12,ti) ; :: thesis: x in {t} *'

then reconsider sj = x as place of (CPNT . j) ;

A42: [ti,sj] in O12 by A41, RELSET_2:9;

[i,j] in XorDelta I by D3;

then [i,j] in dom O by PARTFUN1:def 2;

then O . [i,j] in rng O by FUNCT_1:3;

then [ti,sj] in union (rng O) by D3, A42, TARSKI:def 4;

then reconsider f = [t,sj] as T-S_arc of SCPNT by XBOOLE_0:def 3;

CT1: the carrier of (CPNT . j) = P . j by AS1;

P . j c= P0 by ZFMISC_1:74;

then reconsider s = sj as place of SCPNT by CT1;

A44: f = [t,s] ;

t in {t} by TARSKI:def 1;

hence x in {t} *' by A44; :: thesis: verum

end;assume A41: x in Im (O12,ti) ; :: thesis: x in {t} *'

then reconsider sj = x as place of (CPNT . j) ;

A42: [ti,sj] in O12 by A41, RELSET_2:9;

[i,j] in XorDelta I by D3;

then [i,j] in dom O by PARTFUN1:def 2;

then O . [i,j] in rng O by FUNCT_1:3;

then [ti,sj] in union (rng O) by D3, A42, TARSKI:def 4;

then reconsider f = [t,sj] as T-S_arc of SCPNT by XBOOLE_0:def 3;

CT1: the carrier of (CPNT . j) = P . j by AS1;

P . j c= P0 by ZFMISC_1:74;

then reconsider s = sj as place of SCPNT by CT1;

A44: f = [t,s] ;

t in {t} by TARSKI:def 1;

hence x in {t} *' by A44; :: thesis: verum

the firing-rule of SCPNT . t = UQ . t by AG1, FUNCT_4:13

.= q12 . ti by DF1, D3, LMQ1A ;

then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS0,I0)),(thin_cylinders (CS0,O0)) by v8, CT1, D3;

hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum

take SCPNT ; :: thesis: ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ )

thus ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st

( ( for i being Element of I holds

( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ ) by AS1, AS2, AS3, AS4, AS5, AS6, LL43; :: thesis: verum