let I be non trivial finite set ; for CPNT being Colored-PT-net-Family of I st CPNT is disjoint_valued holds
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )
let CPNT be Colored-PT-net-Family of I; ( CPNT is disjoint_valued implies for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) ) )
assume AS0:
CPNT is disjoint_valued
; for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )
let O be connecting-mapping of CPNT; for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )
let q be connecting-firing-rule of O; ( ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) implies ( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) ) )
assume AS1:
for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2
; ( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )
E1:
for RQ being object st RQ in rng q holds
ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )
proof
let RQ be
object ;
( RQ in rng q implies ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) )
assume
RQ in rng q
;
ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )
then consider z being
object such that E2:
(
z in dom q &
RQ = q . z )
by FUNCT_1:def 3;
z in XorDelta I
by E2;
then consider i,
j being
Element of
I such that E3:
(
z = [i,j] &
i <> j )
;
consider Oij being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j),
qij being
Function such that E4:
(
qij = q . [i,j] &
Oij = O . [i,j] &
dom qij = Outbds (CPNT . i) & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
qij . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) )
by E3, Defcntfir;
qij in Funcs (
(Outbds (CPNT . i)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } ))
by SYLM3, E4;
hence
ex
i,
j being
Element of
I ex
Oij being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) ex
qij being
Function st
(
i <> j & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
qij . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) &
qij in Funcs (
(Outbds (CPNT . i)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) &
RQ = q . [i,j] &
q . [i,j] = qij &
O . [i,j] = Oij )
by E2, E3, E4;
verum
end;
E5:
for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 )
proof
let z be
object ;
( z in union (rng q) implies ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) )
assume
z in union (rng q)
;
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 )
then consider Z being
set such that E6:
(
z in Z &
Z in rng q )
by TARSKI:def 4;
consider i,
j being
Element of
I,
Oij being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j),
qij being
Function such that E8:
(
i <> j & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
qij . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) &
qij in Funcs (
(Outbds (CPNT . i)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) &
Z = q . [i,j] &
q . [i,j] = qij &
O . [i,j] = Oij )
by E1, E6;
thus
ex
i,
j being
Element of
I ex
q12 being
Function ex
O12 being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) st
(
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] &
z in q12 )
by E6, E8;
verum
end;
for z being object st z in union (rng q) holds
ex x, y being object st z = [x,y]
proof
let z be
object ;
( z in union (rng q) implies ex x, y being object st z = [x,y] )
assume
z in union (rng q)
;
ex x, y being object st z = [x,y]
then consider i,
j being
Element of
I,
q12 being
Function,
O12 being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) such that U1:
(
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] &
z in q12 )
by E5;
thus
ex
x,
y being
object st
z = [x,y]
by U1, RELAT_1:def 1;
verum
end;
then reconsider G1 = union (rng q) as Relation by RELAT_1:def 1;
for x, y1, y2 being object st [x,y1] in G1 & [x,y2] in G1 holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in G1 & [x,y2] in G1 implies y1 = y2 )
assume P01:
(
[x,y1] in G1 &
[x,y2] in G1 )
;
y1 = y2
then consider i1,
j1 being
Element of
I,
q121 being
Function,
O121 being
Function of
(Outbds (CPNT . i1)), the
carrier of
(CPNT . j1) such that U11:
(
i1 <> j1 & ( for
t01 being
transition of
(CPNT . i1) st
t01 is
outbound holds
q121 . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))) ) &
q121 in Funcs (
(Outbds (CPNT . i1)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))))) where t01 is transition of (CPNT . i1) : t01 is outbound } )) &
q121 = q . [i1,j1] &
O121 = O . [i1,j1] &
[x,y1] in q121 )
by E5;
consider i2,
j2 being
Element of
I,
q122 being
Function,
O122 being
Function of
(Outbds (CPNT . i2)), the
carrier of
(CPNT . j2) such that U12:
(
i2 <> j2 & ( for
t01 being
transition of
(CPNT . i2) st
t01 is
outbound holds
q122 . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))) ) &
q122 in Funcs (
(Outbds (CPNT . i2)),
(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))))) where t01 is transition of (CPNT . i2) : t01 is outbound } )) &
q122 = q . [i2,j2] &
O122 = O . [i2,j2] &
[x,y2] in q122 )
by E5, P01;
x in dom q121
by U11, XTUPLE_0:def 12;
then s1:
x in Outbds (CPNT . i1)
by U11, FUNCT_2:92;
x in dom q122
by U12, XTUPLE_0:def 12;
then s2:
x in Outbds (CPNT . i2)
by U12, FUNCT_2:92;
i1 = i2
then
[x,y2] in q121
by U12, U11, AS1;
hence
y1 = y2
by U11, FUNCT_1:def 1;
verum
end;
hence
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( 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] & z in q12 ) ) )
by E5, FUNCT_1:def 1; verum