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 P12,T12 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 T12,P12 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 P12,T12 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 T12,P12 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 P12,T12
;
then reconsider ST12 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 as non empty Relation of P12,T12 ;
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 T12,P12
;
then reconsider TTS12 = the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 as non empty Relation of T12,P12 ;
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 CPNT1 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 CPNT2 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 T12,P12 by A15, RELSET_1:17;
the Places of CPNT2 c= P12
by XBOOLE_1:7;
then reconsider E31 = O12 as Relation of T12,P12 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 T12,P12 ;
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 Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #);
( 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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
CPNT1 by A34, TARSKI:def 3;
consider CS1 being non
empty Subset of the
ColoredSet of
CPNT1,
I1 being
Subset of
(*' {t1}),
O1 being
Subset of
({t1} *' ) 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
(*' {t}) 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 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:1;
{t1} *' c= {t} *'
by A25, A26, A27, Th7;
then reconsider O =
O1 as
Subset of
({t} *' ) 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 the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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
CPNT2 by A36, TARSKI:def 3;
consider CS1 being non
empty Subset of the
ColoredSet of
CPNT2,
I1 being
Subset of
(*' {t1}),
O1 being
Subset of
({t1} *' ) 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
(*' {t}) 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 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:1;
{t1} *' c= {t} *'
by A28, A30, A29, Th7;
then reconsider O =
O1 as
Subset of
({t} *' ) 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 the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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)then reconsider t1 =
t as
transition of
CPNT1 by A9;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by A25, A26, A27, Th7;
reconsider CS = the
ColoredSet of
CPNT1 as non
empty Subset of 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;
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
CPNT2 ;
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
({t} *' ) ;
ex
x1 being
transition of
CPNT1 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 the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) 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 the ColoredSet of Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) 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)then reconsider t1 =
t as
transition of
CPNT2 by A10;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by A28, A30, A29, Th7;
reconsider CS = the
ColoredSet of
CPNT2 as non
empty Subset of 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;
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
CPNT1 ;
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
({t} *' ) ;
ex
x1 being
transition of
CPNT2 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 the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) 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 the
ColoredSet of
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) ex
I being
Subset of
(*' {t}) ex
O being
Subset of
({t} *' ) 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #)
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
CPNT1 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) 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
CPNT2 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) 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
CPNT2 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) 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
CPNT1 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
Colored_PT_net_Str(#
P12,
T12,
ST12,
TS12,
CS12,
(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) 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 CPNT1 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 CPNT2 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