reconsider CS12 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 as non empty finite set ;
reconsider T12 = the Transitions of CPNT1 \/ the Transitions of CPNT2 as non empty set ;
reconsider P12 = the Places of CPNT1 \/ the Places of CPNT2 as non empty set ;
A2:
the Transitions of CPNT1 c= T12
by XBOOLE_1:7;
the Places of CPNT1 c= P12
by XBOOLE_1:7;
then reconsider E1 = the S-T_Arcs of CPNT1 as Relation of , by A2, RELSET_1:17;
A3:
the Places of CPNT2 c= P12
by XBOOLE_1:7;
the Transitions of CPNT2 c= T12
by XBOOLE_1:7;
then reconsider E22 = the T-S_Arcs of CPNT2 as Relation of , by A3, RELSET_1:17;
set R1 = the firing-rule of CPNT1;
A4:
the Transitions of CPNT2 c= T12
by XBOOLE_1:7;
the Places of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E2 = the S-T_Arcs of CPNT2 as Relation of , by A4, RELSET_1:17;
set R2 = the firing-rule of CPNT2;
A5:
the Places of CPNT1 c= P12
by XBOOLE_1:7;
the Transitions of CPNT1 c= T12
by XBOOLE_1:7;
then reconsider E21 = the T-S_Arcs of CPNT1 as Relation of , by A5, RELSET_1:17;
A6:
the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
E1 \/ E2 is Relation of ,
;
then reconsider ST12 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 as non empty Relation of , ;
A7:
the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
E21 \/ E22 is Relation of ,
;
then reconsider TTS12 = the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 as non empty Relation of , ;
consider q12, q21 being Function, O12 being Function of Outbds CPNT1,the Places of CPNT2, O21 being Function of Outbds CPNT2,the Places of CPNT1 such that
A8:
O = [O12,O21]
and
A9:
dom q12 = Outbds CPNT1
and
A10:
dom q21 = Outbds CPNT2
and
A11:
for t01 being transition of st t01 is outbound holds
q12 . t01 is Function of thin_cylinders the ColoredSet of CPNT1,(*' {t01}), thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)
and
A12:
for t02 being transition of st t02 is outbound holds
q21 . t02 is Function of thin_cylinders the ColoredSet of CPNT2,(*' {t02}), thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)
and
A13:
q = [q12,q21]
by Def13;
A14:
dom the firing-rule of CPNT2 c= the Transitions of CPNT2 \ (dom q21)
by A10, Def10;
the Transitions of CPNT2 c= T12
by XBOOLE_1:7;
then A15:
Outbds CPNT2 c= T12
by XBOOLE_1:1;
the Transitions of CPNT1 c= T12
by XBOOLE_1:7;
then A16:
Outbds CPNT1 c= T12
by XBOOLE_1:1;
A17:
the Transitions of CPNT1 /\ the Transitions of CPNT2 = {}
by A1, Def11;
A18:
dom the firing-rule of CPNT1 c= the Transitions of CPNT1 \ (dom q12)
by A9, Def10;
then A19:
(dom the firing-rule of CPNT1) /\ (dom the firing-rule of CPNT2) = {}
by A9, A10, A17, A14, Lm6;
A20:
(dom the firing-rule of CPNT2) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A21:
(dom the firing-rule of CPNT2) /\ (dom q12) = {}
by A9, A10, A17, A18, A14, Lm6;
A22:
(dom q12) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A23:
(dom the firing-rule of CPNT1) /\ (dom q21) = {}
by A9, A10, A17, A18, A14, Lm6;
A24:
(dom the firing-rule of CPNT1) /\ (dom q12) = {}
by A9, A10, A17, A18, A14, Lm6;
the Places of CPNT1 c= P12
by XBOOLE_1:7;
then reconsider E32 = O21 as Relation of , by A15, RELSET_1:17;
the Places of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E31 = O12 as Relation of , by A16, RELSET_1:17;
set R4 = q21;
set R3 = q12;
set CR12 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21;
reconsider TS12 = TTS12 \/ (E31 \/ E32) as non empty Relation of , ;
set CPNT12 = Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #);
A25:
the Places of CPNT1 c= the Places of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
A26:
the S-T_Arcs of CPNT1 c= the S-T_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
then A27:
the T-S_Arcs of CPNT1 c= the T-S_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A6, XBOOLE_1:1;
A28:
the Places of CPNT2 c= the Places of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
then A29:
the T-S_Arcs of CPNT2 c= the T-S_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A7, XBOOLE_1:1;
A30:
the S-T_Arcs of CPNT2 c= the S-T_Arcs of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
A32:
for t being transition of st t in dom the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) holds
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,O
proof
let t be
transition of ;
( t in dom the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) implies ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,O )
assume A33:
t in dom the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,O
now per cases
( t in dom the firing-rule of CPNT1 or t in dom the firing-rule of CPNT2 or t in dom q12 or t in dom q21 )
by A31, A33;
suppose A34:
t in dom the
firing-rule of
CPNT1
;
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,O
dom the
firing-rule of
CPNT1 c= the
Transitions of
CPNT1 \ (Outbds CPNT1)
by Def10;
then reconsider t1 =
t as
transition of
by A34, TARSKI:def 3;
consider CS1 being non
empty Subset of ,
I1 being
Subset of ,
O1 being
Subset of
such that A35:
the
firing-rule of
CPNT1 . t1 is
Function of
thin_cylinders CS1,
I1,
thin_cylinders CS1,
O1
by A34, Def10;
*' {t1} c= *' {t}
by A25, A26, A27, Th7;
then reconsider I =
I1 as
Subset of
by XBOOLE_1:1;
the
ColoredSet of
CPNT1 c= the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
then reconsider CS =
CS1 as non
empty Subset of
by XBOOLE_1:1;
{t1} *' c= {t} *'
by A25, A26, A27, Th7;
then reconsider O =
O1 as
Subset of
by XBOOLE_1:1;
the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
by A19, A24, A23, A21, A20, A22, A34, A35, Lm5;
hence
ex
CS being non
empty Subset of ex
I being
Subset of ex
O being
Subset of st the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
;
verum end; suppose A36:
t in dom the
firing-rule of
CPNT2
;
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,O
dom the
firing-rule of
CPNT2 c= the
Transitions of
CPNT2 \ (Outbds CPNT2)
by Def10;
then reconsider t1 =
t as
transition of
by A36, TARSKI:def 3;
consider CS1 being non
empty Subset of ,
I1 being
Subset of ,
O1 being
Subset of
such that A37:
the
firing-rule of
CPNT2 . t1 is
Function of
thin_cylinders CS1,
I1,
thin_cylinders CS1,
O1
by A36, Def10;
*' {t1} c= *' {t}
by A28, A30, A29, Th7;
then reconsider I =
I1 as
Subset of
by XBOOLE_1:1;
the
ColoredSet of
CPNT2 c= the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
then reconsider CS =
CS1 as non
empty Subset of
by XBOOLE_1:1;
{t1} *' c= {t} *'
by A28, A30, A29, Th7;
then reconsider O =
O1 as
Subset of
by XBOOLE_1:1;
the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
by A19, A24, A23, A21, A20, A22, A36, A37, Lm5;
hence
ex
CS being non
empty Subset of ex
I being
Subset of ex
O being
Subset of st the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
;
verum end; suppose A38:
t in dom q12
;
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,Othen reconsider t1 =
t as
transition of
by A9;
reconsider I =
*' {t1} as
Subset of
by A25, A26, A27, Th7;
reconsider CS = the
ColoredSet of
CPNT1 as non
empty Subset of
by XBOOLE_1:7;
Im O12,
t1 c= {t} *'
proof
let x be
set ;
TARSKI:def 3 ( not x in Im O12,t1 or x in {t} *' )
A39:
E31 \/ E32 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
assume A40:
x in Im O12,
t1
;
x in {t} *'
then reconsider s =
x as
place of ;
A41:
[t1,s] in O12
by A40, RELSET_2:9;
O12 c= E31 \/ E32
by XBOOLE_1:7;
then
O12 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A39, XBOOLE_1:1;
then reconsider f =
[t,s] as
T-S_arc of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A41;
A42:
the
Places of
CPNT2 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
A43:
f = [t,s]
;
A44:
t in {t}
by TARSKI:def 1;
s in the
Places of
CPNT2
;
hence
x in {t} *'
by A42, A44, A43;
verum
end; then reconsider O =
Im O12,
t1 as
Subset of ;
ex
x1 being
transition of st
(
t1 = x1 &
x1 is
outbound )
by A9, A38;
then
q12 . t1 is
Function of
thin_cylinders the
ColoredSet of
CPNT1,
(*' {t1}),
thin_cylinders the
ColoredSet of
CPNT1,
(Im O12,t1)
by A11;
then
the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
by A19, A24, A23, A21, A20, A22, A38, Lm5;
hence
ex
CS being non
empty Subset of ex
I being
Subset of ex
O being
Subset of st the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
;
verum end; suppose A45:
t in dom q21
;
ex CS being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) . t is Function of thin_cylinders CS,I, thin_cylinders CS,Othen reconsider t1 =
t as
transition of
by A10;
reconsider I =
*' {t1} as
Subset of
by A28, A30, A29, Th7;
reconsider CS = the
ColoredSet of
CPNT2 as non
empty Subset of
by XBOOLE_1:7;
Im O21,
t1 c= {t} *'
proof
let x be
set ;
TARSKI:def 3 ( not x in Im O21,t1 or x in {t} *' )
A46:
O21 c= E31 \/ E32
by XBOOLE_1:7;
assume A47:
x in Im O21,
t1
;
x in {t} *'
then reconsider s =
x as
place of ;
A48:
E31 \/ E32 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
[t1,s] in O21
by A47, RELSET_2:9;
then reconsider f =
[t,s] as
T-S_arc of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A46, A48, TARSKI:def 3;
A49:
the
Places of
CPNT1 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
A50:
f = [t,s]
;
A51:
t in {t}
by TARSKI:def 1;
s in the
Places of
CPNT1
;
hence
x in {t} *'
by A49, A51, A50;
verum
end; then reconsider O =
Im O21,
t1 as
Subset of ;
ex
x1 being
transition of st
(
t1 = x1 &
x1 is
outbound )
by A10, A45;
then
q21 . t1 is
Function of
thin_cylinders the
ColoredSet of
CPNT2,
(*' {t1}),
thin_cylinders the
ColoredSet of
CPNT2,
(Im O21,t1)
by A12;
then
the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
by A19, A24, A23, A21, A20, A22, A45, Lm5;
hence
ex
CS being non
empty Subset of ex
I being
Subset of ex
O being
Subset of st the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
;
verum end;
hence
ex
CS being non
empty Subset of ex
I being
Subset of ex
O being
Subset of st the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
. t is
Function of
thin_cylinders CS,
I,
thin_cylinders CS,
O
;
verum
end;
A52:
TS12 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21
by XBOOLE_1:4;
then A56:
dom the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) c= the Transitions of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by TARSKI:def 3;
dom the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) c= the Transitions of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) \ (Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #))
proof
set RR4 =
q21;
set RR3 =
q12;
set RR2 = the
firing-rule of
CPNT2;
set RR1 = the
firing-rule of
CPNT1;
let x be
set ;
TARSKI:def 3 ( not x in dom the firing-rule of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) or x in the Transitions of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) \ (Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)) )
assume A57:
x in dom the
firing-rule of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
x in the Transitions of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) \ (Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #))
then reconsider t =
x as
transition of
by A53;
now per cases
( t in dom the firing-rule of CPNT1 or t in dom the firing-rule of CPNT2 or t in dom q12 or t in dom q21 )
by A31, A57;
suppose A58:
t in dom the
firing-rule of
CPNT1
;
not x in Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)A59:
dom the
firing-rule of
CPNT1 c= the
Transitions of
CPNT1 \ (Outbds CPNT1)
by Def10;
then reconsider t1 =
t as
transition of
by A58, XBOOLE_0:def 5;
not
t in Outbds CPNT1
by A58, A59, XBOOLE_0:def 5;
then
not
t1 is
outbound
;
then
{t1} *' <> {}
by Def8;
then A60:
ex
g being
set st
g in {t1} *'
by XBOOLE_0:def 1;
{t1} *' c= {t} *'
by A25, A26, A27, Th7;
then
for
w being
transition of holds
( not
t = w or not
w is
outbound )
by A60, Def8;
hence
not
x in Outbds Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
verum end; suppose A61:
t in dom the
firing-rule of
CPNT2
;
not x in Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)A62:
dom the
firing-rule of
CPNT2 c= the
Transitions of
CPNT2 \ (Outbds CPNT2)
by Def10;
then reconsider t1 =
t as
transition of
by A61, XBOOLE_0:def 5;
not
t in Outbds CPNT2
by A61, A62, XBOOLE_0:def 5;
then
not
t1 is
outbound
;
then
{t1} *' <> {}
by Def8;
then A63:
ex
g being
set st
g in {t1} *'
by XBOOLE_0:def 1;
{t1} *' c= {t} *'
by A28, A30, A29, Th7;
then
for
w being
transition of holds
( not
t = w or not
w is
outbound )
by A63, Def8;
hence
not
x in Outbds Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
verum end; suppose
t in dom q12
;
not x in Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)then
t in dom O12
by A9, FUNCT_2:def 1;
then consider s being
set such that A64:
[t,s] in O12
by RELAT_1:def 4;
reconsider s =
s as
place of
by A64, ZFMISC_1:106;
A65:
E31 \/ E32 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
O12 c= E31 \/ E32
by XBOOLE_1:7;
then
O12 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A65, XBOOLE_1:1;
then reconsider f =
[t,s] as
T-S_arc of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A64;
A66:
the
Places of
CPNT2 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
A67:
f = [t,s]
;
A68:
t in {t}
by TARSKI:def 1;
s in the
Places of
CPNT2
;
then
s in {t} *'
by A66, A68, A67;
then
for
w being
transition of holds
( not
t = w or not
w is
outbound )
by Def8;
hence
not
x in Outbds Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
verum end; suppose
t in dom q21
;
not x in Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)then
t in dom O21
by A10, FUNCT_2:def 1;
then consider s being
set such that A69:
[t,s] in O21
by RELAT_1:def 4;
reconsider s =
s as
place of
by A69, ZFMISC_1:106;
A70:
E31 \/ E32 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by XBOOLE_1:7;
O21 c= E31 \/ E32
by XBOOLE_1:7;
then
O21 c= the
T-S_Arcs of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A70, XBOOLE_1:1;
then reconsider f =
[t,s] as
T-S_arc of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
by A69;
A71:
the
Places of
CPNT1 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
A72:
f = [t,s]
;
A73:
t in {t}
by TARSKI:def 1;
s in the
Places of
CPNT1
;
then
s in {t} *'
by A71, A73, A72;
then
for
w being
transition of holds
( not
t = w or not
w is
outbound )
by Def8;
hence
not
x in Outbds Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
;
verum end;
hence
x in the
Transitions of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
\ (Outbds Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #))
by A56, A57, XBOOLE_0:def 5;
verum
end;
then
Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) is Colored-PT-net-like
by A32, Def10;
hence
ex b1 being strict Colored-PT-net ex q12, q21 being Function ex O12 being Function of Outbds CPNT1,the Places of CPNT2 ex O21 being Function of Outbds CPNT2,the Places of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( for t01 being transition of st t01 is outbound holds
q12 . t01 is Function of thin_cylinders the ColoredSet of CPNT1,(*' {t01}), thin_cylinders the ColoredSet of CPNT1,(Im O12,t01) ) & ( for t02 being transition of st t02 is outbound holds
q21 . t02 is Function of thin_cylinders the ColoredSet of CPNT2,(*' {t02}), thin_cylinders the ColoredSet of CPNT2,(Im O21,t02) ) & q = [q12,q21] & the Places of b1 = the Places of CPNT1 \/ the Places of CPNT2 & the Transitions of b1 = the Transitions of CPNT1 \/ the Transitions of CPNT2 & the S-T_Arcs of b1 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b1 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b1 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b1 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 )
by A8, A9, A10, A11, A12, A13, A52; verum