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