theorem SYLM3:
for
CPNT1,
CPNT2 being
Colored-PT-net for
O12 being
Function of
(Outbds CPNT1), the
carrier of
CPNT2 for
q12 being
Function st
dom q12 = Outbds CPNT1 & ( 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)))) ) holds
q12 in Funcs (
(Outbds CPNT1),
(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ))