deffunc H1( Element of I, Element of I) -> set = { (Funcs ((Outbds (CPNT . $1)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . $1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . $1),(Im (O12,t01)))))) where t01 is transition of (CPNT . $1) : t01 is outbound } ))) where O12 is Function of (Outbds (CPNT . $1)), the carrier of (CPNT . $2) : O . [$1,$2] = O12 } ;
R1:
for i, j being Element of I
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in union H1(i,j)
proof
let i,
j be
Element of
I;
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in union H1(i,j)let Oij be
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j);
for q being Function st Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in union H1(i,j)let q be
Function;
( Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) implies q in union H1(i,j) )
assume A1:
(
Oij = O . [i,j] &
dom q = Outbds (CPNT . i) & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
q . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) )
;
q in union H1(i,j)
P1:
q 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, A1;
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 } ))
in H1(
i,
j)
by A1;
hence
q in union H1(
i,
j)
by P1, TARSKI:def 4;
verum
end;
consider i0, j0 being Element of I such that
I0J0:
i0 <> j0
by LMXorDelta;
reconsider Oi0j0 = O . [i0,j0] as Function of (Outbds (CPNT . i0)), the carrier of (CPNT . j0) by I0J0, Defcntmap;
reconsider Oj0i0 = O . [j0,i0] as Function of (Outbds (CPNT . j0)), the carrier of (CPNT . i0) by I0J0, Defcntmap;
reconsider O0 = [Oi0j0,Oj0i0] as connecting-mapping of CPNT . i0,CPNT . j0 by PETRI_2:def 13;
set q0 = the connecting-firing-rule of CPNT . i0,CPNT . j0,O0;
consider q12, q21 being Function, O12 being Function of (Outbds (CPNT . i0)), the carrier of (CPNT . j0), O21 being Function of (Outbds (CPNT . j0)), the carrier of (CPNT . i0) such that
X0:
( O0 = [O12,O21] & dom q12 = Outbds (CPNT . i0) & dom q21 = Outbds (CPNT . j0) & ( for t01 being transition of (CPNT . i0) st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i0),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i0),(Im (O12,t01)))) ) & ( for t02 being transition of (CPNT . j0) st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of (CPNT . j0),(*' {t02}))),(thin_cylinders ( the ColoredSet of (CPNT . j0),(Im (O21,t02)))) ) & the connecting-firing-rule of CPNT . i0,CPNT . j0,O0 = [q12,q21] )
by PETRI_2:def 14;
x1: Oi0j0 =
O0 `1
.=
O12
by X0
;
union H1(i0,j0) in { (union H1(i,j)) where i, j is Element of I : i <> j }
by I0J0;
then
union H1(i0,j0) c= union { (union H1(i,j)) where i, j is Element of I : i <> j }
by ZFMISC_1:74;
then reconsider Y = union { (union H1(i,j)) where i, j is Element of I : i <> j } as non empty set by x1, X0, R1;
R2:
for i, j being Element of I
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in Y
proof
let i,
j be
Element of
I;
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in Ylet Oij be
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j);
for q being Function st i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in Ylet q be
Function;
( i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) implies q in Y )
assume A1:
(
i <> j &
Oij = O . [i,j] &
dom q = Outbds (CPNT . i) & ( for
t01 being
transition of
(CPNT . i) st
t01 is
outbound holds
q . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) )
;
q in Y
then A2:
q in union H1(
i,
j)
by R1;
union H1(
i,
j)
in { (union H1(i,j)) where i, j is Element of I : i <> j }
by A1;
hence
q in Y
by A2, TARSKI:def 4;
verum
end;
defpred S1[ object , object ] means 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
( $1 = [i,j] & Oij = O . [i,j] & qij = $2 & 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)))) ) );
P1:
for x being object st x in XorDelta I holds
ex y being object st
( y in Y & S1[x,y] )
proof
let x be
object ;
( x in XorDelta I implies ex y being object st
( y in Y & S1[x,y] ) )
assume
x in XorDelta I
;
ex y being object st
( y in Y & S1[x,y] )
then consider i,
j being
Element of
I such that P11:
(
x = [i,j] &
i <> j )
;
reconsider Oij =
O . [i,j] as
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) by P11, Defcntmap;
reconsider Oji =
O . [j,i] as
Function of
(Outbds (CPNT . j)), the
carrier of
(CPNT . i) by P11, Defcntmap;
reconsider O0 =
[Oij,Oji] as
connecting-mapping of
CPNT . i,
CPNT . j by PETRI_2:def 13;
set q0 = the
connecting-firing-rule of
CPNT . i,
CPNT . j,
O0;
consider q12,
q21 being
Function,
O12 being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j),
O21 being
Function of
(Outbds (CPNT . j)), the
carrier of
(CPNT . i) such that X0:
(
O0 = [O12,O21] &
dom q12 = Outbds (CPNT . i) &
dom q21 = Outbds (CPNT . 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)))) ) & ( for
t02 being
transition of
(CPNT . j) st
t02 is
outbound holds
q21 . t02 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . j),(*' {t02}))),
(thin_cylinders ( the ColoredSet of (CPNT . j),(Im (O21,t02)))) ) & the
connecting-firing-rule of
CPNT . i,
CPNT . j,
O0 = [q12,q21] )
by PETRI_2:def 14;
Oij =
O0 `1
.=
O12
by X0
;
hence
ex
y being
object st
(
y in Y &
S1[
x,
y] )
by X0, P11, R2;
verum
end;
consider f being Function of (XorDelta I),Y such that
P2:
for x being object st x in XorDelta I holds
S1[x,f . x]
from FUNCT_2:sch 1(P1);
reconsider f = f as ManySortedSet of XorDelta I ;
take
f
; for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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)))) ) )
thus
for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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)))) ) )
verumproof
let i,
j be
Element of
I;
( i <> j implies ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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)))) ) ) )
assume
i <> j
;
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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)))) ) )
then p04:
[i,j] in XorDelta I
;
consider i1,
j1 being
Element of
I,
Oij being
Function of
(Outbds (CPNT . i1)), the
carrier of
(CPNT . j1),
qij being
Function such that P4:
(
[i,j] = [i1,j1] &
Oij = O . [i1,j1] &
qij = f . [i,j] &
i1 <> j1 &
dom qij = Outbds (CPNT . i1) & ( for
t01 being
transition of
(CPNT . i1) st
t01 is
outbound holds
qij . t01 is
Function of
(thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),
(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (Oij,t01)))) ) )
by p04, P2;
(
i = i1 &
j = j1 )
by XTUPLE_0:1, P4;
hence
ex
Oij being
Function of
(Outbds (CPNT . i)), the
carrier of
(CPNT . j) ex
qij being
Function st
(
qij = f . [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 P4;
verum
end;