set L2 = bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2);
set L1 = bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2);
set K2 = bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1);
set K1 = bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1);
set TO2 = Outbds CPNT2;
set TO1 = Outbds CPNT1;
set Y1 = PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1));
set Y2 = PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2));
consider O12 being Function of (Outbds CPNT1),the Places of CPNT2, O21 being Function of (Outbds CPNT2),the Places of CPNT1 such that
A1:
O = [O12,O21]
by Def12;
defpred S1[ set , set ] means ex t02 being transition of CPNT2 st
( $1 = t02 & $2 is Function of (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) );
defpred S2[ set , set ] means ex t01 being transition of CPNT1 st
( $1 = t01 & $2 is Function of (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) );
A2:
for x being set st x in Outbds CPNT1 holds
ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)) & S2[x,y] )
proof
let x be
set ;
( x in Outbds CPNT1 implies ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)) & S2[x,y] ) )
assume
x in Outbds CPNT1
;
ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)) & S2[x,y] )
then consider t01 being
transition of
CPNT1 such that A3:
x = t01
and
t01 is
outbound
;
set t2 =
Im O12,
t01;
set t1 =
*' {t01};
consider y being
Function of
(thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01));
take
y
;
( y in PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)) & S2[x,y] )
set H1 =
thin_cylinders the
ColoredSet of
CPNT1,
(*' {t01});
set H2 =
thin_cylinders the
ColoredSet of
CPNT1,
(Im O12,t01);
A4:
Funcs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) c= PFuncs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01))
by FUNCT_2:141;
A5:
thin_cylinders the
ColoredSet of
CPNT1,
(Im O12,t01) c= bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)
by Lm1;
thin_cylinders the
ColoredSet of
CPNT1,
(*' {t01}) c= bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)
by Lm1;
then A6:
PFuncs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) c= PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),
(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1))
by A5, PARTFUN1:128;
y in Funcs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01))
by FUNCT_2:11;
then
y in PFuncs (thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01))
by A4;
hence
(
y in PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),
(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1)) &
S2[
x,
y] )
by A3, A6;
verum
end;
consider q12 being Function of (Outbds CPNT1),(PFuncs (bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT1)),(bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT1))) such that
A7:
for x being set st x in Outbds CPNT1 holds
S2[x,q12 . x]
from FUNCT_2:sch 1(A2);
A8:
now let tt01 be
transition of
CPNT1;
( tt01 is outbound implies q12 . tt01 is Function of (thin_cylinders the ColoredSet of CPNT1,(*' {tt01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,tt01)) )assume
tt01 is
outbound
;
q12 . tt01 is Function of (thin_cylinders the ColoredSet of CPNT1,(*' {tt01})),(thin_cylinders the ColoredSet of CPNT1,(Im O12,tt01))then
tt01 in Outbds CPNT1
;
then
ex
t01 being
transition of
CPNT1 st
(
tt01 = t01 &
q12 . tt01 is
Function of
(thin_cylinders the ColoredSet of CPNT1,(*' {t01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,t01)) )
by A7;
hence
q12 . tt01 is
Function of
(thin_cylinders the ColoredSet of CPNT1,(*' {tt01})),
(thin_cylinders the ColoredSet of CPNT1,(Im O12,tt01))
;
verum end;
A9:
for x being set st x in Outbds CPNT2 holds
ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)) & S1[x,y] )
proof
let x be
set ;
( x in Outbds CPNT2 implies ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)) & S1[x,y] ) )
assume
x in Outbds CPNT2
;
ex y being set st
( y in PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)) & S1[x,y] )
then consider t02 being
transition of
CPNT2 such that A10:
x = t02
and
t02 is
outbound
;
set t2 =
Im O21,
t02;
set t1 =
*' {t02};
consider y being
Function of
(thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02));
take
y
;
( y in PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)) & S1[x,y] )
set H1 =
thin_cylinders the
ColoredSet of
CPNT2,
(*' {t02});
set H2 =
thin_cylinders the
ColoredSet of
CPNT2,
(Im O21,t02);
A11:
Funcs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) c= PFuncs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02))
by FUNCT_2:141;
A12:
thin_cylinders the
ColoredSet of
CPNT2,
(Im O21,t02) c= bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)
by Lm1;
thin_cylinders the
ColoredSet of
CPNT2,
(*' {t02}) c= bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)
by Lm1;
then A13:
PFuncs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) c= PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),
(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2))
by A12, PARTFUN1:128;
y in Funcs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02))
by FUNCT_2:11;
then
y in PFuncs (thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02))
by A11;
hence
(
y in PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),
(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2)) &
S1[
x,
y] )
by A10, A13;
verum
end;
consider q21 being Function of (Outbds CPNT2),(PFuncs (bool (PFuncs the Places of CPNT2,the ColoredSet of CPNT2)),(bool (PFuncs the Places of CPNT1,the ColoredSet of CPNT2))) such that
A14:
for x being set st x in Outbds CPNT2 holds
S1[x,q21 . x]
from FUNCT_2:sch 1(A9);
A15:
now let tt02 be
transition of
CPNT2;
( tt02 is outbound implies q21 . tt02 is Function of (thin_cylinders the ColoredSet of CPNT2,(*' {tt02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,tt02)) )assume
tt02 is
outbound
;
q21 . tt02 is Function of (thin_cylinders the ColoredSet of CPNT2,(*' {tt02})),(thin_cylinders the ColoredSet of CPNT2,(Im O21,tt02))then
tt02 in Outbds CPNT2
;
then
ex
t02 being
transition of
CPNT2 st
(
tt02 = t02 &
q21 . tt02 is
Function of
(thin_cylinders the ColoredSet of CPNT2,(*' {t02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,t02)) )
by A14;
hence
q21 . tt02 is
Function of
(thin_cylinders the ColoredSet of CPNT2,(*' {tt02})),
(thin_cylinders the ColoredSet of CPNT2,(Im O21,tt02))
;
verum end;
take
[q12,q21]
; 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)) ) & [q12,q21] = [q12,q21] )
A16:
dom q21 = Outbds CPNT2
by FUNCT_2:def 1;
dom q12 = Outbds CPNT1
by FUNCT_2:def 1;
hence
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)) ) & [q12,q21] = [q12,q21] )
by A1, A8, A15, A16; verum