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
P1:
( 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] )
by Def9;
reconsider P12 = the Places of CPNT1 \/ the Places of CPNT2 as non empty set ;
reconsider T12 = the Transitions of CPNT1 \/ the Transitions of CPNT2 as non empty set ;
( the Places of CPNT1 c= P12 & the Transitions of CPNT1 c= T12 )
by XBOOLE_1:7;
then reconsider E1 = the S-T_Arcs of CPNT1 as Relation of P12,T12 by RELSET_1:17;
( the Places of CPNT2 c= P12 & the Transitions of CPNT2 c= T12 )
by XBOOLE_1:7;
then reconsider E2 = the S-T_Arcs of CPNT2 as Relation of P12,T12 by RELSET_1:17;
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 ;
( the Transitions of CPNT1 c= T12 & the Places of CPNT1 c= P12 )
by XBOOLE_1:7;
then reconsider E21 = the T-S_Arcs of CPNT1 as Relation of T12,P12 by RELSET_1:17;
( the Transitions of CPNT2 c= T12 & the Places of CPNT2 c= P12 )
by XBOOLE_1:7;
then reconsider E22 = the T-S_Arcs of CPNT2 as Relation of T12,P12 by RELSET_1:17;
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 ;
the Transitions of CPNT1 c= T12
by XBOOLE_1:7;
then L30:
Outbds CPNT1 c= T12
by XBOOLE_1:1;
the Transitions of CPNT2 c= T12
by XBOOLE_1:7;
then L31:
Outbds CPNT2 c= T12
by XBOOLE_1:1;
L32:
the Places of CPNT2 c= P12
by XBOOLE_1:7;
L33:
the Places of CPNT1 c= P12
by XBOOLE_1:7;
reconsider E31 = O12 as Relation of T12,P12 by L30, L32, RELSET_1:17;
reconsider E32 = O21 as Relation of T12,P12 by L31, L33, RELSET_1:17;
reconsider TS12 = TTS12 \/ (E31 \/ E32) as non empty Relation of T12,P12 ;
reconsider CS12 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 as non empty finite set ;
set CR12 = ((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21;
set CPNT12 = Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,(((the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #);
set R1 = the firing-rule of CPNT1;
set R2 = the firing-rule of CPNT2;
set R3 = q12;
set R4 = q21;
P2:
TS12 = ((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21
by XBOOLE_1:4;
LM6T1:
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;
LM6T2:
the Transitions of CPNT1 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 XBOOLE_1:7;
LM6T3:
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;
Q2:
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;
the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
then LM6T4:
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 Q2, XBOOLE_1:1;
LM6S1:
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;
LM6S2:
the Transitions of CPNT2 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 XBOOLE_1:7;
LM6S3:
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;
Q2:
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;
the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2
by XBOOLE_1:7;
then LM6S4:
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 Q2, XBOOLE_1:1;
LM7T1:
the Transitions of CPNT1 /\ the Transitions of CPNT2 = {}
by AS, Def7A;
LM7T4:
dom the firing-rule of CPNT1 c= the Transitions of CPNT1 \ (dom q12)
by P1, Def4;
LM7T5:
dom the firing-rule of CPNT2 c= the Transitions of CPNT2 \ (dom q21)
by P1, Def4;
LM7T:
( (dom the firing-rule of CPNT1) /\ (dom the firing-rule of CPNT2) = {} & (dom the firing-rule of CPNT1) /\ (dom the firing-rule of CPNT2) = {} & (dom the firing-rule of CPNT1) /\ (dom q12) = {} & (dom the firing-rule of CPNT1) /\ (dom q21) = {} & (dom the firing-rule of CPNT2) /\ (dom q12) = {} & (dom the firing-rule of CPNT2) /\ (dom q21) = {} & (dom q12) /\ (dom q21) = {} )
by LM8, LM7T1, P1, LM7T4, LM7T5;
then S10:
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;
SS1:
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) #);
:: thesis: ( 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 SS2:
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) #)
;
:: thesis: 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 SS2, P22;
suppose S4:
t in dom the
firing-rule of
CPNT1
;
:: thesis: 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 Def4;
then reconsider t1 =
t as
transition of
CPNT1 by S4, 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 T6:
the
firing-rule of
CPNT1 . t1 is
Function of
(thin_cylinders CS1,I1),
(thin_cylinders CS1,O1)
by Def4, S4;
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 LM6, LM6T1, LM6T2, LM6T3, LM6T4;
then reconsider I =
I1 as
Subset of
(*' {t}) by XBOOLE_1:1;
{t1} *' c= {t} *'
by LM6, LM6T1, LM6T2, LM6T3, LM6T4;
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 S4, LM7, LM7T, T6;
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)
;
:: thesis: verum end; suppose S5:
t in dom the
firing-rule of
CPNT2
;
:: thesis: 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 Def4;
then reconsider t1 =
t as
transition of
CPNT2 by S5, 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 T6:
the
firing-rule of
CPNT2 . t1 is
Function of
(thin_cylinders CS1,I1),
(thin_cylinders CS1,O1)
by Def4, S5;
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 LM6, LM6S1, LM6S2, LM6S3, LM6S4;
then reconsider I =
I1 as
Subset of
(*' {t}) by XBOOLE_1:1;
{t1} *' c= {t} *'
by LM6, LM6S1, LM6S2, LM6S3, LM6S4;
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 S5, LM7, LM7T, T6;
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)
;
:: thesis: verum end; suppose S6:
t in dom q12
;
:: thesis: 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)reconsider t1 =
t as
transition of
CPNT1 by S6, P1;
S610:
ex
x1 being
transition of
CPNT1 st
(
t1 = x1 &
x1 is
outbound )
by S6, P1;
T6:
q12 . t1 is
Function of
(thin_cylinders the ColoredSet of CPNT1,(*' {t1})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t1))
by P1, S610;
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;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by LM6, LM6T1, LM6T2, LM6T3, LM6T4;
Im O12,
t1 c= {t} *'
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Im O12,t1 or x in {t} *' )
assume Z:
x in Im O12,
t1
;
:: thesis: x in {t} *'
then reconsider s =
x as
place of
CPNT2 ;
A1:
[t1,s] in O12
by Z, RELSET_2:9;
A5:
O12 c= E31 \/ E32
by XBOOLE_1:7;
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;
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 A5, 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 A1;
A4:
s in the
Places of
CPNT2
;
A31:
the
Places of
CPNT2 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
(
t in {t} &
f = [t,s] )
by TARSKI:def 1;
hence
x in {t} *'
by A31, A4;
:: thesis: verum
end; then reconsider O =
Im O12,
t1 as
Subset of
({t} *' ) ;
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 S6, LM7, LM7T, T6;
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)
;
:: thesis: verum end; suppose S7:
t in dom q21
;
:: thesis: 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 P1;
S610:
ex
x1 being
transition of
CPNT2 st
(
t1 = x1 &
x1 is
outbound )
by S7, P1;
T6:
q21 . t1 is
Function of
(thin_cylinders the ColoredSet of CPNT2,(*' {t1})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t1))
by P1, S610;
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;
reconsider I =
*' {t1} as
Subset of
(*' {t}) by LM6, LM6S1, LM6S2, LM6S3, LM6S4;
Im O21,
t1 c= {t} *'
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Im O21,t1 or x in {t} *' )
assume Z:
x in Im O21,
t1
;
:: thesis: x in {t} *'
then reconsider s =
x as
place of
CPNT1 ;
A1:
[t1,s] in O21
by Z, RELSET_2:9;
A5:
O21 c= E31 \/ E32
by XBOOLE_1:7;
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;
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 A1, A5, TARSKI:def 3;
A4:
s in the
Places of
CPNT1
;
A31:
the
Places of
CPNT1 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
(
t in {t} &
f = [t,s] )
by TARSKI:def 1;
hence
x in {t} *'
by A31, A4;
:: thesis: verum
end; then reconsider O =
Im O21,
t1 as
Subset of
({t} *' ) ;
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 S7, LM7, LM7T, T6;
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)
;
:: thesis: 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)
;
:: thesis: verum
end;
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
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ASD:
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) #)
;
:: thesis: 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 s10;
set RR1 = the
firing-rule of
CPNT1;
set RR2 = the
firing-rule of
CPNT2;
set RR3 =
q12;
set RR4 =
q21;
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 ASD, P22;
suppose CAS1:
t in dom the
firing-rule of
CPNT1
;
:: thesis: 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) #)Q0:
dom the
firing-rule of
CPNT1 c= the
Transitions of
CPNT1 \ (Outbds CPNT1)
by Def4;
then Q1:
(
t in the
Transitions of
CPNT1 & not
t in Outbds CPNT1 )
by CAS1, XBOOLE_0:def 5;
reconsider t1 =
t as
transition of
CPNT1 by Q0, CAS1, XBOOLE_0:def 5;
not
t1 is
outbound
by Q1;
then
{t1} *' <> {}
by Def7;
then Q2:
ex
g being
set st
g in {t1} *'
by XBOOLE_0:def 1;
{t1} *' c= {t} *'
by LM6, LM6T1, LM6T2, LM6T3, LM6T4;
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 Def7, Q2;
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) #)
;
:: thesis: verum end; suppose CAS2:
t in dom the
firing-rule of
CPNT2
;
:: thesis: 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) #)Q0:
dom the
firing-rule of
CPNT2 c= the
Transitions of
CPNT2 \ (Outbds CPNT2)
by Def4;
then Q1:
(
t in the
Transitions of
CPNT2 & not
t in Outbds CPNT2 )
by CAS2, XBOOLE_0:def 5;
reconsider t1 =
t as
transition of
CPNT2 by Q0, CAS2, XBOOLE_0:def 5;
not
t1 is
outbound
by Q1;
then
{t1} *' <> {}
by Def7;
then Q2:
ex
g being
set st
g in {t1} *'
by XBOOLE_0:def 1;
{t1} *' c= {t} *'
by LM6, LM6S1, LM6S2, LM6S3, LM6S4;
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 Def7, Q2;
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) #)
;
:: thesis: verum end; suppose CAS3:
t in dom q12
;
:: thesis: 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) #)
t in dom O12
by P1, CAS3, FUNCT_2:def 1;
then consider s being
set such that FF:
[t,s] in O12
by RELAT_1:def 4;
reconsider s =
s as
place of
CPNT2 by FF, ZFMISC_1:106;
A5:
O12 c= E31 \/ E32
by XBOOLE_1:7;
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;
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 A5, 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 FF;
A4:
s in the
Places of
CPNT2
;
A31:
the
Places of
CPNT2 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
(
t in {t} &
f = [t,s] )
by TARSKI:def 1;
then
s in {t} *'
by A4, A31;
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 Def7;
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) #)
;
:: thesis: verum end; suppose CAS4:
t in dom q21
;
:: thesis: 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) #)
t in dom O21
by P1, CAS4, FUNCT_2:def 1;
then consider s being
set such that FF:
[t,s] in O21
by RELAT_1:def 4;
reconsider s =
s as
place of
CPNT1 by FF, ZFMISC_1:106;
A5:
O21 c= E31 \/ E32
by XBOOLE_1:7;
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;
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 A5, 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 FF;
A4:
s in the
Places of
CPNT1
;
A31:
the
Places of
CPNT1 c= the
Places of
CPNT1 \/ the
Places of
CPNT2
by XBOOLE_1:7;
(
t in {t} &
f = [t,s] )
by TARSKI:def 1;
then
s in {t} *'
by A31, A4;
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 Def7;
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) #)
;
:: thesis: 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 ASD, S10, XBOOLE_0:def 5;
:: thesis: 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 SS1, Def4;
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 P1, P2; :: thesis: verum