:: PETRI_2 semantic presentation

begin

definition
let A be non empty set ;
let B, Bo be set ;
let yo be Function of Bo,A;
assume A1: Bo c= B ;
func cylinder0 (A,B,Bo,yo) ->  non empty Subset of (Funcs (B,A)) equals :Def1: :: PETRI_2:def 1
 {  y where y is Function of B,A : y | Bo = yo  }  ;
correctness
coherence
{  y where y is Function of B,A : y | Bo = yo  }  is non empty Subset of (Funcs (B,A));
proof
set D =  {  y where y is Function of B,A : y | Bo = yo  }  ;
A2: now__::_thesis:_not__{__y_where_y_is_Function_of_B,A_:_y_|_Bo_=_yo__}__is_empty
percases ( Bo = {} or Bo <> {} ) ;
supposeA3: Bo = {} ; ::_thesis: not  {  y where y is Function of B,A : y | Bo = yo  }  is empty
set f = the Function of B,A;
the Function of B,A | {} = {}
.= yo by A3 ;
then  the Function of B,A in  {  y where y is Function of B,A : y | Bo = yo  }  by A3;
hence  not  {  y where y is Function of B,A : y | Bo = yo  }  is empty ; ::_thesis: verum
end;
suppose Bo <> {} ; ::_thesis: not  {  y where y is Function of B,A : y | Bo = yo  }  is empty
then consider b0 being set  such that
A4: b0 in Bo by XBOOLE_0:def_1;
 yo . b0 in A by A4, FUNCT_2:5;
then A5: {(yo . b0)} c= A by ZFMISC_1:31;
set f = (B --> (yo . b0)) +* yo;
A6: rng ((B --> (yo . b0)) +* yo) c= (rng (B --> (yo . b0))) \/ (rng yo) by FUNCT_4:17;
A7: rng yo c= A by RELAT_1:def_19;
A8: dom yo = Bo by FUNCT_2:def_1;
then A9: dom ((B --> (yo . b0)) +* yo) = (dom (B --> (yo . b0))) \/ Bo by FUNCT_4:def_1
.= B \/ Bo by FUNCOP_1:13
.= B by A1, XBOOLE_1:12 ;
 rng (B --> (yo . b0)) c= {(yo . b0)} by FUNCOP_1:13;
then  rng (B --> (yo . b0)) c= A by A5, XBOOLE_1:1;
then  (rng (B --> (yo . b0))) \/ (rng yo) c= A by A7, XBOOLE_1:8;
then reconsider f = (B --> (yo . b0)) +* yo as Function of B,A by A6, A9, FUNCT_2:2, XBOOLE_1:1;
 f | Bo = yo by A8, FUNCT_4:23;
then  f in  {  y where y is Function of B,A : y | Bo = yo  }  ;
hence  not  {  y where y is Function of B,A : y | Bo = yo  }  is empty ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_z_being_set_st_z_in__{__y_where_y_is_Function_of_B,A_:_y_|_Bo_=_yo__}__holds_
z_in_Funcs_(B,A)
let z be set ; ::_thesis: ( z in  {  y where y is Function of B,A : y | Bo = yo  }  implies z in Funcs (B,A) )
assume  z in  {  y where y is Function of B,A : y | Bo = yo  }  ; ::_thesis: z in Funcs (B,A)
then  ex y being Function of B,A st
( z = y & y | Bo = yo ) ;
hence  z in Funcs (B,A) by FUNCT_2:8; ::_thesis: verum
end;
hence   {  y where y is Function of B,A : y | Bo = yo  }  is non empty Subset of (Funcs (B,A)) by A2, TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines cylinder0 PETRI_2:def_1_:_
 for A being non empty set
for B, Bo being set
for yo being Function of Bo,A st Bo c= B holds
cylinder0 (A,B,Bo,yo) =  {  y where y is Function of B,A : y | Bo = yo  }  ;

definition
let A be non empty set ;
let B be set ;
mode thin_cylinder of A,B ->  non empty Subset of (Funcs (B,A)) means :Def2: :: PETRI_2:def 2
 ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & it = cylinder0 (A,B,Bo,yo) );
existence
 ex b1 being non empty Subset of (Funcs (B,A)) ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & b1 = cylinder0 (A,B,Bo,yo) )
proof
set Bo = {} ;
set yo = the Function of {},A;
take  cylinder0 (A,B,{}, the Function of {},A) ; ::_thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{}, the Function of {},A) = cylinder0 (A,B,Bo,yo) )
 {} is Subset of B by XBOOLE_1:2;
hence  ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{}, the Function of {},A) = cylinder0 (A,B,Bo,yo) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines thin_cylinder PETRI_2:def_2_:_
 for A being non empty set
for B being set
for b3 being non empty Subset of (Funcs (B,A)) holds
( b3 is thin_cylinder of A,B iff ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & b3 = cylinder0 (A,B,Bo,yo) ) );

theorem Th1: :: PETRI_2:1
for A being non empty set
for B being set
for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  )
proof
let A be non empty set ; ::_thesis: for B being set
for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  )
let B be set ; ::_thesis: for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  )
let D be thin_cylinder of A,B; ::_thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  )
consider Bo being Subset of B, yo being Function of Bo,A such that
A1: Bo is finite and
A2: D = cylinder0 (A,B,Bo,yo) by Def2;
 D =  {  y where y is Function of B,A : y | Bo = yo  }  by A2, Def1;
hence  ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  ) by A1; ::_thesis: verum
end;

theorem :: PETRI_2:2
for A1, A2 being non empty set
for B being set
for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
proof
let A1, A2 be non empty set ; ::_thesis: for B being set
for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
let B be set ; ::_thesis: for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
let D1 be thin_cylinder of A1,B; ::_thesis: ( A1 c= A2 implies ex D2 being thin_cylinder of A2,B st D1 c= D2 )
consider Bo being Subset of B, yo1 being Function of Bo,A1 such that
A1: Bo is finite and
A2: D1 =  {  y where y is Function of B,A1 : y | Bo = yo1  }  by Th1;
assume A3: A1 c= A2 ; ::_thesis: ex D2 being thin_cylinder of A2,B st D1 c= D2
then reconsider yo2 = yo1 as Function of Bo,A2 by FUNCT_2:7;
set D2 =  {  y where y is Function of B,A2 : y | Bo = yo2  }  ;
A4: now__::_thesis:_for_x_being_set_st_x_in_D1_holds_
x_in__{__y_where_y_is_Function_of_B,A2_:_y_|_Bo_=_yo2__}_
let x be set ; ::_thesis: ( x in D1 implies x in  {  y where y is Function of B,A2 : y | Bo = yo2  }  )
assume  x in D1 ; ::_thesis: x in  {  y where y is Function of B,A2 : y | Bo = yo2  }
then consider y1 being Function of B,A1 such that
A5: x = y1 and
A6: y1 | Bo = yo1 by A2;
reconsider y2 = y1 as Function of B,A2 by A3, FUNCT_2:7;
 y2 | Bo = yo1 by A6;
hence  x in  {  y where y is Function of B,A2 : y | Bo = yo2  }  by A5; ::_thesis: verum
end;
  {  y where y is Function of B,A2 : y | Bo = yo2  }  = cylinder0 (A2,B,Bo,yo2) by Def1;
then reconsider D2 =  {  y where y is Function of B,A2 : y | Bo = yo2  }  as thin_cylinder of A2,B by A1, Def2;
take  D2 ; ::_thesis: D1 c= D2
thus  D1 c= D2 by A4, TARSKI:def_3; ::_thesis: verum
end;

definition
let A be non empty set ;
let B be set ;
func thin_cylinders (A,B) ->  non empty Subset-Family of (Funcs (B,A)) equals :: PETRI_2:def 3
 {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  ;
correctness
coherence
{  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  is non empty Subset-Family of (Funcs (B,A));
proof
set F = the thin_cylinder of A,B;
A1: now__::_thesis:_for_z_being_set_st_z_in__{__D_where_D_is_Subset_of_(Funcs_(B,A))_:_D_is_thin_cylinder_of_A,B__}__holds_
z_in_bool_(Funcs_(B,A))
let z be set ; ::_thesis: ( z in  {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  implies z in bool (Funcs (B,A)) )
assume  z in  {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  ; ::_thesis: z in bool (Funcs (B,A))
then  ex D being Subset of (Funcs (B,A)) st
( z = D & D is thin_cylinder of A,B ) ;
hence  z in bool (Funcs (B,A)) ; ::_thesis: verum
end;
 the thin_cylinder of A,B in  {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  ;
hence   {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  is non empty Subset-Family of (Funcs (B,A)) by A1, TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines thin_cylinders PETRI_2:def_3_:_
 for A being non empty set
for B being set holds thin_cylinders (A,B) =  {  D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B  }  ;

Lm1:  for A being non empty set
for B, C being set st B c= C holds
thin_cylinders (A,B) c= bool (PFuncs (C,A))
proof
let A be non empty set ; ::_thesis: for B, C being set st B c= C holds
thin_cylinders (A,B) c= bool (PFuncs (C,A))
let B, C be set ; ::_thesis: ( B c= C implies thin_cylinders (A,B) c= bool (PFuncs (C,A)) )
assume  B c= C ; ::_thesis: thin_cylinders (A,B) c= bool (PFuncs (C,A))
then A1: PFuncs (B,A) c= PFuncs (C,A) by PARTFUN1:50;
 Funcs (B,A) c= PFuncs (B,A) by FUNCT_2:72;
then  Funcs (B,A) c= PFuncs (C,A) by A1, XBOOLE_1:1;
then A2: bool (Funcs (B,A)) c= bool (PFuncs (C,A)) by ZFMISC_1:67;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in thin_cylinders (A,B) or x in bool (PFuncs (C,A)) )
assume  x in thin_cylinders (A,B) ; ::_thesis: x in bool (PFuncs (C,A))
then consider D being Subset of (Funcs (B,A)) such that
A3: x = D and
 D is thin_cylinder of A,B ;
 D in bool (Funcs (B,A)) ;
hence  x in bool (PFuncs (C,A)) by A3, A2; ::_thesis: verum
end;

Lm2:  for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
proof
let A be non trivial set ; ::_thesis: for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let B be set ; ::_thesis: for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let Bo1, Bo2 be Subset of B; ::_thesis: for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let yo1 be Function of Bo1,A; ::_thesis: for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let yo2 be Function of Bo2,A; ::_thesis: ( not Bo2 c= Bo1 implies ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 ) )
defpred S1[ set ] means $1 in Bo1;
deffunc H1( set ) ->  set = yo1 . $1;
assume  not Bo2 c= Bo1 ; ::_thesis: ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
then consider x0 being set  such that
A1: x0 in Bo2 and
A2: not x0 in Bo1 by TARSKI:def_3;
A3: x0 in dom yo2 by A1, FUNCT_2:def_1;
 ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )
proof
consider x, y being set  such that
A4: x in A and
A5: y in A and
A6: x <> y by ZFMISC_1:def_10;
percases ( yo2 . x0 = x or yo2 . x0 <> x ) ;
supposeA7: yo2 . x0 = x ; ::_thesis: ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )
take  y ; ::_thesis: ( y in A & y <> yo2 . x0 )
thus  ( y in A & y <> yo2 . x0 ) by A5, A6, A7; ::_thesis: verum
end;
supposeA8: yo2 . x0 <> x ; ::_thesis: ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )
take  x ; ::_thesis: ( x in A & x <> yo2 . x0 )
thus  ( x in A & x <> yo2 . x0 ) by A4, A8; ::_thesis: verum
end;
end;
end;
then consider y0 being set  such that
A9: y0 in A and
A10: y0 <> yo2 . x0 ;
deffunc H2( set ) ->  set = y0;
A11: for x being set st x in B holds
( ( S1[x] implies H1(x) in A ) & ( not S1[x] implies H2(x) in A ) ) by A9, FUNCT_2:5;
consider f being Function of B,A such that
A12: for x being set st x in B holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch_5(A11);
A13: now__::_thesis:_for_z_being_set_st_z_in_dom_yo1_holds_
yo1_._z_=_f_._z
let z be set ; ::_thesis: ( z in dom yo1 implies yo1 . z = f . z )
assume  z in dom yo1 ; ::_thesis: yo1 . z = f . z
then  z in Bo1 ;
hence  yo1 . z = f . z by A12; ::_thesis: verum
end;
 f . x0 <> yo2 . x0 by A1, A2, A10, A12;
then A14: f | Bo2 <> yo2 by A3, FUNCT_1:47;
dom yo1 = Bo1 by FUNCT_2:def_1
.= B /\ Bo1 by XBOOLE_1:28
.= (dom f) /\ Bo1 by FUNCT_2:def_1 ;
then  f | Bo1 = yo1 by A13, FUNCT_1:46;
hence  ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 ) by A14; ::_thesis: verum
end;

Lm3:  for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
proof
let A be non trivial set ; ::_thesis: for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let B be set ; ::_thesis: for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let Bo1, Bo2 be Subset of B; ::_thesis: for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let yo1 be Function of Bo1,A; ::_thesis: for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let yo2 be Function of Bo2,A; ::_thesis: ( Bo1 <> Bo2 & Bo2 c= Bo1 implies ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 ) )
assume that
A1: Bo1 <> Bo2 and
A2: Bo2 c= Bo1 ; ::_thesis: ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
 Bo2 c< Bo1 by A1, A2, XBOOLE_0:def_8;
then consider x0 being set  such that
A3: x0 in Bo1 and
A4: not x0 in Bo2 by XBOOLE_0:6;
A5: x0 in dom yo1 by A3, FUNCT_2:def_1;
deffunc H1( set ) ->  set = yo2 . $1;
defpred S1[ set ] means $1 in Bo2;
 ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
proof
consider x, y being set  such that
A6: x in A and
A7: y in A and
A8: x <> y by ZFMISC_1:def_10;
percases ( yo1 . x0 = x or yo1 . x0 <> x ) ;
supposeA9: yo1 . x0 = x ; ::_thesis: ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
take  y ; ::_thesis: ( y in A & y <> yo1 . x0 )
thus  ( y in A & y <> yo1 . x0 ) by A7, A8, A9; ::_thesis: verum
end;
supposeA10: yo1 . x0 <> x ; ::_thesis: ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
take  x ; ::_thesis: ( x in A & x <> yo1 . x0 )
thus  ( x in A & x <> yo1 . x0 ) by A6, A10; ::_thesis: verum
end;
end;
end;
then consider y0 being set  such that
A11: y0 in A and
A12: y0 <> yo1 . x0 ;
deffunc H2( set ) ->  set = y0;
A13: for x being set st x in B holds
( ( S1[x] implies H1(x) in A ) & ( not S1[x] implies H2(x) in A ) ) by A11, FUNCT_2:5;
consider f being Function of B,A such that
A14: for x being set st x in B holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch_5(A13);
A15: now__::_thesis:_for_z_being_set_st_z_in_dom_yo2_holds_
yo2_._z_=_f_._z
let z be set ; ::_thesis: ( z in dom yo2 implies yo2 . z = f . z )
assume  z in dom yo2 ; ::_thesis: yo2 . z = f . z
then  z in Bo2 ;
hence  yo2 . z = f . z by A14; ::_thesis: verum
end;
 f . x0 <> yo1 . x0 by A3, A4, A12, A14;
then A16: f | Bo1 <> yo1 by A5, FUNCT_1:47;
dom yo2 = Bo2 by FUNCT_2:def_1
.= B /\ Bo2 by XBOOLE_1:28
.= (dom f) /\ Bo2 by FUNCT_2:def_1 ;
then  f | Bo2 = yo2 by A15, FUNCT_1:46;
hence  ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 ) by A16; ::_thesis: verum
end;

Lm4:  for A being non trivial set
for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
proof
let A be non trivial set ; ::_thesis: for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
let B be set ; ::_thesis: for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
let Bo1, Bo2 be Subset of B; ::_thesis: for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
let yo1 be Function of Bo1,A; ::_thesis: for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
let yo2 be Function of Bo2,A; ::_thesis: ( Bo1 <> Bo2 implies  {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }  )
assume A1: Bo1 <> Bo2 ; ::_thesis:  {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
percases ( not Bo2 c= Bo1 or Bo2 c= Bo1 ) ;
suppose not Bo2 c= Bo1 ; ::_thesis:  {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
then consider f being Function of B,A such that
A2: f | Bo1 = yo1 and
A3: f | Bo2 <> yo2 by Lm2;
 not f in  {  y where y is Function of B,A : y | Bo2 = yo2  }
proof
assume  f in  {  y where y is Function of B,A : y | Bo2 = yo2  }  ; ::_thesis: contradiction
then  ex y being Function of B,A st
( f = y & y | Bo2 = yo2 ) ;
hence  contradiction by A3; ::_thesis: verum
end;
hence   {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }  by A2; ::_thesis: verum
end;
suppose Bo2 c= Bo1 ; ::_thesis:  {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }
then consider f being Function of B,A such that
A4: f | Bo2 = yo2 and
A5: f | Bo1 <> yo1 by A1, Lm3;
 not f in  {  y where y is Function of B,A : y | Bo1 = yo1  }
proof
assume  f in  {  y where y is Function of B,A : y | Bo1 = yo1  }  ; ::_thesis: contradiction
then  ex y being Function of B,A st
( f = y & y | Bo1 = yo1 ) ;
hence  contradiction by A5; ::_thesis: verum
end;
hence   {  y where y is Function of B,A : y | Bo1 = yo1  }  <>  {  y where y is Function of B,A : y | Bo2 = yo2  }  by A4; ::_thesis: verum
end;
end;
end;

theorem Th3: :: PETRI_2:3
for A being non trivial set
for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
proof
let A be non trivial set ; ::_thesis: for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
let B, Bo1 be set ; ::_thesis: for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
let yo1 be Function of Bo1,A; ::_thesis: for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
let Bo2 be set ; ::_thesis: for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) holds
( Bo1 = Bo2 & yo1 = yo2 )
let yo2 be Function of Bo2,A; ::_thesis: ( Bo1 c= B & Bo2 c= B & cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) implies ( Bo1 = Bo2 & yo1 = yo2 ) )
assume that
A1: Bo1 c= B and
A2: Bo2 c= B and
A3: cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) ; ::_thesis: ( Bo1 = Bo2 & yo1 = yo2 )
A4:  {  y where y is Function of B,A : y | Bo1 = yo1  }  = cylinder0 (A,B,Bo1,yo1) by A1, Def1;
then consider y0 being set  such that
A5: y0 in  {  y where y is Function of B,A : y | Bo1 = yo1  }  by XBOOLE_0:def_1;
A6: ex y being Function of B,A st
( y0 = y & y | Bo1 = yo1 ) by A5;
A7:  {  y where y is Function of B,A : y | Bo2 = yo2  }  = cylinder0 (A,B,Bo2,yo2) by A2, Def1;
hence  Bo1 = Bo2 by A1, A2, A3, A4, Lm4; ::_thesis: yo1 = yo2
 ex w being Function of B,A st
( y0 = w & w | Bo2 = yo2 ) by A3, A4, A7, A5;
hence  yo1 = yo2 by A1, A2, A3, A4, A7, A6, Lm4; ::_thesis: verum
end;

theorem Th4: :: PETRI_2:4
for A1, A2 being non empty set
for B1, B2 being set st A1 c= A2 & B1 c= B2 holds
ex F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) )
proof
let A1, A2 be non empty set ; ::_thesis: for B1, B2 being set st A1 c= A2 & B1 c= B2 holds
ex F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) )
let B1, B2 be set ; ::_thesis: ( A1 c= A2 & B1 c= B2 implies ex F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) ) )
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ; ::_thesis: ex F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) )
defpred S1[ set , set ] means  ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & $1 = cylinder0 (A1,B1,Bo,yo1) & $2 = cylinder0 (A2,B2,Bo,yo2) );
A3: now__::_thesis:_for_x_being_set_st_x_in_thin_cylinders_(A1,B1)_holds_
ex_D2_being_set_st_
(_D2_in_thin_cylinders_(A2,B2)_&_S1[x,D2]_)
let x be set ; ::_thesis: ( x in thin_cylinders (A1,B1) implies ex D2 being set st
( D2 in thin_cylinders (A2,B2) & S1[x,D2] ) )
assume  x in thin_cylinders (A1,B1) ; ::_thesis: ex D2 being set st
( D2 in thin_cylinders (A2,B2) & S1[x,D2] )
then  ex D being Subset of (Funcs (B1,A1)) st
( x = D & D is thin_cylinder of A1,B1 ) ;
then reconsider D1 = x as thin_cylinder of A1,B1 ;
consider Bo being Subset of B1, yo1 being Function of Bo,A1 such that
A4: Bo is finite and
A5: D1 = cylinder0 (A1,B1,Bo,yo1) by Def2;
reconsider yo2 = yo1 as Function of Bo,A2 by A1, FUNCT_2:7;
set D2 = cylinder0 (A2,B2,Bo,yo2);
 Bo c= B2 by A2, XBOOLE_1:1;
then A6: cylinder0 (A2,B2,Bo,yo2) is thin_cylinder of A2,B2 by A4, Def2;
reconsider D2 = cylinder0 (A2,B2,Bo,yo2) as set ;
take D2 = D2; ::_thesis: ( D2 in thin_cylinders (A2,B2) & S1[x,D2] )
thus  ( D2 in thin_cylinders (A2,B2) & S1[x,D2] ) by A4, A5, A6; ::_thesis: verum
end;
consider F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) such that
A7: for x being set st x in thin_cylinders (A1,B1) holds
S1[x,F . x] from FUNCT_2:sch_1(A3);
take  F ; ::_thesis: for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) )
thus  for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F . x = cylinder0 (A2,B2,Bo,yo2) ) by A7; ::_thesis: verum
end;

theorem Th5: :: PETRI_2:5
for A1, A2 being non empty set
for B1, B2 being set ex G being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) )
proof
let A1, A2 be non empty set ; ::_thesis: for B1, B2 being set ex G being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) )
let B1, B2 be set ; ::_thesis: ex G being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) )
defpred S1[ set , set ] means  ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & $1 = cylinder0 (A2,B2,Bo2,yo2) & $2 = cylinder0 (A1,B1,Bo1,yo1) );
A1: now__::_thesis:_for_x_being_set_st_x_in_thin_cylinders_(A2,B2)_holds_
ex_D1_being_set_st_
(_D1_in_thin_cylinders_(A1,B1)_&_S1[x,D1]_)
let x be set ; ::_thesis: ( x in thin_cylinders (A2,B2) implies ex D1 being set st
( D1 in thin_cylinders (A1,B1) & S1[x,D1] ) )
assume  x in thin_cylinders (A2,B2) ; ::_thesis: ex D1 being set st
( D1 in thin_cylinders (A1,B1) & S1[x,D1] )
then  ex D being Subset of (Funcs (B2,A2)) st
( x = D & D is thin_cylinder of A2,B2 ) ;
then reconsider D2 = x as thin_cylinder of A2,B2 ;
consider Bo2 being Subset of B2, yo2 being Function of Bo2,A2 such that
A2: Bo2 is finite and
A3: D2 = cylinder0 (A2,B2,Bo2,yo2) by Def2;
set Bo1 = (B1 /\ Bo2) /\ (yo2 " A1);
A4: (B1 /\ Bo2) /\ (yo2 " A1) c= B1 /\ Bo2 by XBOOLE_1:17;
set yo1 = yo2 | ((B1 /\ Bo2) /\ (yo2 " A1));
 B1 /\ Bo2 c= Bo2 by XBOOLE_1:17;
then  (B1 /\ Bo2) /\ (yo2 " A1) c= Bo2 by A4, XBOOLE_1:1;
then A5: yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) is Function of ((B1 /\ Bo2) /\ (yo2 " A1)),A2 by FUNCT_2:32;
A6: rng (yo2 | ((B1 /\ Bo2) /\ (yo2 " A1))) = yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) by RELAT_1:115;
A7: yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= yo2 .: (yo2 " A1) by RELAT_1:123, XBOOLE_1:17;
 yo2 .: (yo2 " A1) c= A1 by FUNCT_1:75;
then  yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= A1 by A7, XBOOLE_1:1;
then reconsider yo1 = yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) as Function of ((B1 /\ Bo2) /\ (yo2 " A1)),A1 by A5, A6, FUNCT_2:6;
set D1 = cylinder0 (A1,B1,((B1 /\ Bo2) /\ (yo2 " A1)),yo1);
 B1 /\ Bo2 c= B1 by XBOOLE_1:17;
then A8: (B1 /\ Bo2) /\ (yo2 " A1) c= B1 by A4, XBOOLE_1:1;
then A9: cylinder0 (A1,B1,((B1 /\ Bo2) /\ (yo2 " A1)),yo1) is thin_cylinder of A1,B1 by A2, Def2;
reconsider D1 = cylinder0 (A1,B1,((B1 /\ Bo2) /\ (yo2 " A1)),yo1) as set ;
take D1 = D1; ::_thesis: ( D1 in thin_cylinders (A1,B1) & S1[x,D1] )
thus  ( D1 in thin_cylinders (A1,B1) & S1[x,D1] ) by A2, A3, A8, A9; ::_thesis: verum
end;
consider G being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) such that
A10: for x being set st x in thin_cylinders (A2,B2) holds
S1[x,G . x] from FUNCT_2:sch_1(A1);
take  G ; ::_thesis: for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) )
thus  for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & G . x = cylinder0 (A1,B1,Bo1,yo1) ) by A10; ::_thesis: verum
end;

definition
let A1, A2 be non trivial set ;
let B1, B2 be set ;
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ;
func Extcylinders (A1,B1,A2,B2) ->  Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) means :: PETRI_2:def 4
 for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & it . x = cylinder0 (A2,B2,Bo,yo2) );
existence
 ex b1 being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st
for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & b1 . x = cylinder0 (A2,B2,Bo,yo2) ) by A1, A2, Th4;
uniqueness
 for b1, b2 being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) st ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & b1 . x = cylinder0 (A2,B2,Bo,yo2) ) ) & ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & b2 . x = cylinder0 (A2,B2,Bo,yo2) ) ) holds
b1 = b2
proof
let F1, F2 be Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)); ::_thesis: ( ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F1 . x = cylinder0 (A2,B2,Bo,yo2) ) ) & ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ) implies F1 = F2 )
assume A3: for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F1 . x = cylinder0 (A2,B2,Bo,yo2) ) ; ::_thesis: ( ex x being set st
( x in thin_cylinders (A1,B1) & ( for Bo being Subset of B1
for yo1 being Function of Bo,A1
for yo2 being Function of Bo,A2 holds
( not Bo is finite or not yo1 = yo2 or not x = cylinder0 (A1,B1,Bo,yo1) or not F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ) ) or F1 = F2 )
assume A4: for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_st_x_in_thin_cylinders_(A1,B1)_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in thin_cylinders (A1,B1) implies F1 . x = F2 . x )
assume A5: x in thin_cylinders (A1,B1) ; ::_thesis: F1 . x = F2 . x
then consider Bo1 being Subset of B1, yo11 being Function of Bo1,A1, yo21 being Function of Bo1,A2 such that
 Bo1 is finite and
A6: yo11 = yo21 and
A7: x = cylinder0 (A1,B1,Bo1,yo11) and
A8: F1 . x = cylinder0 (A2,B2,Bo1,yo21) by A3;
consider Bo2 being Subset of B1, yo12 being Function of Bo2,A1, yo22 being Function of Bo2,A2 such that
 Bo2 is finite and
A9: yo12 = yo22 and
A10: x = cylinder0 (A1,B1,Bo2,yo12) and
A11: F2 . x = cylinder0 (A2,B2,Bo2,yo22) by A4, A5;
 Bo1 = Bo2 by A7, A10, Th3;
hence  F1 . x = F2 . x by A6, A7, A8, A9, A10, A11, Th3; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem  defines Extcylinders PETRI_2:def_4_:_
 for A1, A2 being non trivial set
for B1, B2 being set st A1 c= A2 & B1 c= B2 holds
for b5 being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) holds
( b5 = Extcylinders (A1,B1,A2,B2) iff for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & b5 . x = cylinder0 (A2,B2,Bo,yo2) ) );

definition
let A1 be non empty set ;
let A2 be non trivial set ;
let B1, B2 be set ;
func Ristcylinders (A1,B1,A2,B2) ->  Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) means :: PETRI_2:def 5
 for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & it . x = cylinder0 (A1,B1,Bo1,yo1) );
existence
 ex b1 being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st
for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & b1 . x = cylinder0 (A1,B1,Bo1,yo1) ) by Th5;
uniqueness
 for b1, b2 being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) st ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & b1 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) & ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & b2 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) holds
b1 = b2
proof
let F1, F2 be Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)); ::_thesis: ( ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & F1 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) & ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & F2 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) implies F1 = F2 )
assume A1: for x being set st x in thin_cylinders (A2,B2) holds
ex Bo21 being Subset of B2 ex Bo11 being Subset of B1 ex yo11 being Function of Bo11,A1 ex yo21 being Function of Bo21,A2 st
( Bo11 is finite & Bo21 is finite & Bo11 = (B1 /\ Bo21) /\ (yo21 " A1) & yo11 = yo21 | Bo11 & x = cylinder0 (A2,B2,Bo21,yo21) & F1 . x = cylinder0 (A1,B1,Bo11,yo11) ) ; ::_thesis: ( ex x being set st
( x in thin_cylinders (A2,B2) & ( for Bo2 being Subset of B2
for Bo1 being Subset of B1
for yo1 being Function of Bo1,A1
for yo2 being Function of Bo2,A2 holds
( not Bo1 is finite or not Bo2 is finite or not Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) or not yo1 = yo2 | Bo1 or not x = cylinder0 (A2,B2,Bo2,yo2) or not F2 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) ) or F1 = F2 )
assume A2: for x being set st x in thin_cylinders (A2,B2) holds
ex Bo22 being Subset of B2 ex Bo12 being Subset of B1 ex yo12 being Function of Bo12,A1 ex yo22 being Function of Bo22,A2 st
( Bo12 is finite & Bo22 is finite & Bo12 = (B1 /\ Bo22) /\ (yo22 " A1) & yo12 = yo22 | Bo12 & x = cylinder0 (A2,B2,Bo22,yo22) & F2 . x = cylinder0 (A1,B1,Bo12,yo12) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_st_x_in_thin_cylinders_(A2,B2)_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in thin_cylinders (A2,B2) implies F1 . x = F2 . x )
assume A3: x in thin_cylinders (A2,B2) ; ::_thesis: F1 . x = F2 . x
then consider Bo21 being Subset of B2, Bo11 being Subset of B1, yo11 being Function of Bo11,A1, yo21 being Function of Bo21,A2 such that
 Bo11 is finite and
 Bo21 is finite and
A4: Bo11 = (B1 /\ Bo21) /\ (yo21 " A1) and
A5: yo11 = yo21 | Bo11 and
A6: x = cylinder0 (A2,B2,Bo21,yo21) and
A7: F1 . x = cylinder0 (A1,B1,Bo11,yo11) by A1;
consider Bo22 being Subset of B2, Bo12 being Subset of B1, yo12 being Function of Bo12,A1, yo22 being Function of Bo22,A2 such that
 Bo12 is finite and
 Bo22 is finite and
A8: Bo12 = (B1 /\ Bo22) /\ (yo22 " A1) and
A9: yo12 = yo22 | Bo12 and
A10: x = cylinder0 (A2,B2,Bo22,yo22) and
A11: F2 . x = cylinder0 (A1,B1,Bo12,yo12) by A2, A3;
A12: yo21 = yo22 by A6, A10, Th3;
 Bo21 = Bo22 by A6, A10, Th3;
hence  F1 . x = F2 . x by A4, A5, A7, A8, A9, A11, A12; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem  defines Ristcylinders PETRI_2:def_5_:_
 for A1 being non empty set
for A2 being non trivial set
for B1, B2 being set
for b5 being Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)) holds
( b5 = Ristcylinders (A1,B1,A2,B2) iff for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & b5 . x = cylinder0 (A1,B1,Bo1,yo1) ) );

definition
let A be non trivial set ;
let B be set ;
let D be thin_cylinder of A,B;
func loc D ->  finite Subset of B means :: PETRI_2:def 6
 ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & it = Bo );
existence
 ex b1 being finite Subset of B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & b1 = Bo )
proof
 ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  ) by Th1;
hence  ex b1 being finite Subset of B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & b1 = Bo ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being finite Subset of B st ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & b1 = Bo ) & ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & b2 = Bo ) holds
b1 = b2 by Lm4;
end;

:: deftheorem  defines loc PETRI_2:def_6_:_
 for A being non trivial set
for B being set
for D being thin_cylinder of A,B
for b4 being finite Subset of B holds
( b4 = loc D iff ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D =  {  y where y is Function of B,A : y | Bo = yo  }  & b4 = Bo ) );

begin

definition
let A1, A2 be non trivial set ;
let B1, B2 be set ;
let C1, C2 be non trivial set ;
let D1, D2 be set ;
let F be Function of (thin_cylinders (A1,B1)),(thin_cylinders (C1,D1));
func CylinderFunc (A1,B1,A2,B2,C1,D1,C2,D2,F) ->  Function of (thin_cylinders (A2,B2)),(thin_cylinders (C2,D2)) equals :: PETRI_2:def 7
((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2));
correctness
coherence
((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2)) is Function of (thin_cylinders (A2,B2)),(thin_cylinders (C2,D2));
;
end;

:: deftheorem  defines CylinderFunc PETRI_2:def_7_:_
 for A1, A2 being non trivial set
for B1, B2 being set
for C1, C2 being non trivial set
for D1, D2 being set
for F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (C1,D1)) holds CylinderFunc (A1,B1,A2,B2,C1,D1,C2,D2,F) = ((Extcylinders (C1,D1,C2,D2)) * F) * (Ristcylinders (A1,B1,A2,B2));

definition
attrc1 is strict ;
struct Colored_PT_net_Str  ->  PT_net_Str ;
aggrColored_PT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs, ColoredSet, firing-rule #) ->  Colored_PT_net_Str ;
sel ColoredSet c1 ->  non empty finite set ;
sel firing-rule c1 ->  Function;
end;

definition
func TrivialColoredPetriNet  ->  Colored_PT_net_Str  equals :: PETRI_2:def 8
 Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);
coherence
 Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #) is Colored_PT_net_Str ;
end;

:: deftheorem  defines TrivialColoredPetriNet PETRI_2:def_8_:_
 TrivialColoredPetriNet = Colored_PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})),{{}},{} #);

registration
cluster TrivialColoredPetriNet  ->  non empty non void with_S-T_arc with_T-S_arc ;
coherence
 ( TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
proof
set N = TrivialColoredPetriNet ;
thus  not the S-T_Arcs of TrivialColoredPetriNet is empty ; :: according to PETRI:def_1 ::_thesis: ( TrivialColoredPetriNet is with_T-S_arc & not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
thus  not the T-S_Arcs of TrivialColoredPetriNet is empty ; :: according to PETRI:def_2 ::_thesis: ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void )
thus  ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void ) ; ::_thesis: verum
end;
end;

registration
cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str ;
existence
 ex b1 being Colored_PT_net_Str st
( not b1 is empty & not b1 is void & b1 is with_S-T_arc & b1 is with_T-S_arc )
proof
take  TrivialColoredPetriNet ; ::_thesis: ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void & TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc )
thus  ( not TrivialColoredPetriNet is empty & not TrivialColoredPetriNet is void & TrivialColoredPetriNet is with_S-T_arc & TrivialColoredPetriNet is with_T-S_arc ) ; ::_thesis: verum
end;
end;

definition
mode Colored_Petri_net is non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str ;
end;

definition
let CPNT be Colored_Petri_net;
let t0 be transition of CPNT;
attrt0 is outbound  means :Def9: :: PETRI_2:def 9
{t0} *' = {} ;
end;

:: deftheorem Def9 defines outbound PETRI_2:def_9_:_
 for CPNT being Colored_Petri_net
for t0 being transition of CPNT holds
( t0 is outbound iff {t0} *' = {} );

definition
let CPNT1 be Colored_Petri_net;
func Outbds CPNT1 ->  Subset of the carrier' of CPNT1 equals :: PETRI_2:def 10
 {  x where x is transition of CPNT1 : x is outbound  }  ;
coherence
  {  x where x is transition of CPNT1 : x is outbound  }  is Subset of the carrier' of CPNT1
proof
  {  x where x is transition of CPNT1 : x is outbound  }  c= the carrier' of CPNT1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is transition of CPNT1 : x is outbound  }  or z in the carrier' of CPNT1 )
assume  z in  {  x where x is transition of CPNT1 : x is outbound  }  ; ::_thesis: z in the carrier' of CPNT1
then  ex x being transition of CPNT1 st
( z = x & x is outbound ) ;
hence  z in the carrier' of CPNT1 ; ::_thesis: verum
end;
hence   {  x where x is transition of CPNT1 : x is outbound  }  is Subset of the carrier' of CPNT1 ; ::_thesis: verum
end;
end;

:: deftheorem  defines Outbds PETRI_2:def_10_:_
 for CPNT1 being Colored_Petri_net holds Outbds CPNT1 =  {  x where x is transition of CPNT1 : x is outbound  }  ;

definition
let CPNT be Colored_Petri_net;
attrCPNT is Colored-PT-net-like  means :Def11: :: PETRI_2:def 11
( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) );
end;

:: deftheorem Def11 defines Colored-PT-net-like PETRI_2:def_11_:_
 for CPNT being Colored_Petri_net holds
( CPNT is Colored-PT-net-like iff ( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) ) );

theorem :: PETRI_2:6
for CPNT being Colored_Petri_net
for t being transition of CPNT st CPNT is Colored-PT-net-like & t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by Def11;

theorem Th7: :: PETRI_2:7
for CPNT1, CPNT2 being Colored_Petri_net
for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
proof
let CPNT1, CPNT2 be Colored_Petri_net; ::_thesis: for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
let t1 be transition of CPNT1; ::_thesis: for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
let t2 be transition of CPNT2; ::_thesis: ( the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 implies ( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' ) )
assume that
A1: the carrier of CPNT1 c= the carrier of CPNT2 and
A2: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 and
A3: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 and
A4: t1 = t2 ; ::_thesis: ( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
thus  *' {t1} c= *' {t2} ::_thesis: {t1} *' c= {t2} *'
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in *' {t1} or x in *' {t2} )
assume A5: x in *' {t1} ; ::_thesis: x in *' {t2}
then A6: x is place of CPNT2 by A1, TARSKI:def_3;
 ex s being place of CPNT1 st
( x = s & ex f being S-T_arc of CPNT1 ex w being transition of CPNT1 st
( w in {t1} & f = [s,w] ) ) by A5;
then consider f being S-T_arc of CPNT1, w being transition of CPNT1 such that
A7: w in {t2} and
A8: f = [x,w] by A4;
 f is S-T_arc of CPNT2 by A2, TARSKI:def_3;
hence  x in *' {t2} by A7, A8, A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {t1} *' or x in {t2} *' )
assume A9: x in {t1} *' ; ::_thesis: x in {t2} *'
then A10: x is place of CPNT2 by A1, TARSKI:def_3;
 ex s being place of CPNT1 st
( x = s & ex f being T-S_arc of CPNT1 ex w being transition of CPNT1 st
( w in {t1} & f = [w,s] ) ) by A9;
then consider f being T-S_arc of CPNT1, w being transition of CPNT1 such that
A11: w in {t2} and
A12: f = [w,x] by A4;
 f is T-S_arc of CPNT2 by A3, TARSKI:def_3;
hence  x in {t2} *' by A11, A12, A10; ::_thesis: verum
end;

Lm5:  for f1, f2, f3, f4, g being Function st (dom f1) /\ (dom f2) = {} & (dom f1) /\ (dom f3) = {} & (dom f1) /\ (dom f4) = {} & (dom f2) /\ (dom f3) = {} & (dom f2) /\ (dom f4) = {} & (dom f3) /\ (dom f4) = {} & g = ((f1 +* f2) +* f3) +* f4 holds
( ( for x being set st x in dom f1 holds
g . x = f1 . x ) & ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )
proof
let f1, f2, f3, f4, g be Function; ::_thesis: ( (dom f1) /\ (dom f2) = {} & (dom f1) /\ (dom f3) = {} & (dom f1) /\ (dom f4) = {} & (dom f2) /\ (dom f3) = {} & (dom f2) /\ (dom f4) = {} & (dom f3) /\ (dom f4) = {} & g = ((f1 +* f2) +* f3) +* f4 implies ( ( for x being set st x in dom f1 holds
g . x = f1 . x ) & ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) ) )
assume that
A1: (dom f1) /\ (dom f2) = {} and
A2: (dom f1) /\ (dom f3) = {} and
A3: (dom f1) /\ (dom f4) = {} and
A4: (dom f2) /\ (dom f3) = {} and
A5: (dom f2) /\ (dom f4) = {} and
A6: (dom f3) /\ (dom f4) = {} and
A7: g = ((f1 +* f2) +* f3) +* f4 ; ::_thesis: ( ( for x being set st x in dom f1 holds
g . x = f1 . x ) & ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )
set f123 = (f1 +* f2) +* f3;
set f12 = f1 +* f2;
thus  for x being set st x in dom f1 holds
g . x = f1 . x ::_thesis: ( ( for x being set st x in dom f2 holds
g . x = f2 . x ) & ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )
proof
let x be set ; ::_thesis: ( x in dom f1 implies g . x = f1 . x )
assume A8: x in dom f1 ; ::_thesis: g . x = f1 . x
then A9: not x in dom f3 by A2, XBOOLE_0:def_4;
A10: not x in dom f2 by A1, A8, XBOOLE_0:def_4;
 not x in dom f4 by A3, A8, XBOOLE_0:def_4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= (f1 +* f2) . x by A9, FUNCT_4:11
.= f1 . x by A10, FUNCT_4:11 ;
::_thesis: verum
end;
thus  for x being set st x in dom f2 holds
g . x = f2 . x ::_thesis: ( ( for x being set st x in dom f3 holds
g . x = f3 . x ) & ( for x being set st x in dom f4 holds
g . x = f4 . x ) )
proof
let x be set ; ::_thesis: ( x in dom f2 implies g . x = f2 . x )
assume A11: x in dom f2 ; ::_thesis: g . x = f2 . x
then A12: not x in dom f3 by A4, XBOOLE_0:def_4;
 not x in dom f4 by A5, A11, XBOOLE_0:def_4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= (f1 +* f2) . x by A12, FUNCT_4:11
.= f2 . x by A11, FUNCT_4:13 ;
::_thesis: verum
end;
thus  for x being set st x in dom f3 holds
g . x = f3 . x ::_thesis: for x being set st x in dom f4 holds
g . x = f4 . x
proof
let x be set ; ::_thesis: ( x in dom f3 implies g . x = f3 . x )
assume A13: x in dom f3 ; ::_thesis: g . x = f3 . x
then  not x in dom f4 by A6, XBOOLE_0:def_4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= f3 . x by A13, FUNCT_4:13 ;
::_thesis: verum
end;
thus  for x being set st x in dom f4 holds
g . x = f4 . x by A7, FUNCT_4:13; ::_thesis: verum
end;

Lm6:  for A, B, C, D, X1, X2, X3, X4 being set st A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D holds
( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
proof
let A, B, C, D, X1, X2, X3, X4 be set ; ::_thesis: ( A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D implies ( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} ) )
assume that
A1: A /\ B = {} and
A2: C c= A and
A3: D c= B and
A4: X1 c= A \ C and
A5: X2 c= B \ D and
A6: X3 = C and
A7: X4 = D ; ::_thesis: ( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
A8: (A \ C) /\ (B \ D) c= A /\ B by XBOOLE_1:27;
 X1 /\ X2 c= (A \ C) /\ (B \ D) by A4, A5, XBOOLE_1:27;
hence  X1 /\ X2 = {} by A1, A8; ::_thesis: ( X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
A9: C /\ A c= C by XBOOLE_1:17;
 (A \ C) /\ C = (C /\ A) \ C by XBOOLE_1:49;
then  (A \ C) /\ C = {} by A9, XBOOLE_1:37;
hence  X1 /\ X3 = {} by A4, A6, XBOOLE_1:3, XBOOLE_1:27; ::_thesis: ( X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
 (A \ C) /\ D = {} by A1, A3, XBOOLE_1:3, XBOOLE_1:27;
hence  X1 /\ X4 = {} by A4, A7, XBOOLE_1:3, XBOOLE_1:27; ::_thesis: ( X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
 (B \ D) /\ C = {} by A1, A2, XBOOLE_1:3, XBOOLE_1:27;
hence  X2 /\ X3 = {} by A5, A6, XBOOLE_1:3, XBOOLE_1:27; ::_thesis: ( X2 /\ X4 = {} & X3 /\ X4 = {} )
A10: B /\ D c= D by XBOOLE_1:17;
 (B \ D) /\ D = (B /\ D) \ D by XBOOLE_1:49;
then  (B \ D) /\ D = {} by A10, XBOOLE_1:37;
hence  X2 /\ X4 = {} by A5, A7, XBOOLE_1:3, XBOOLE_1:27; ::_thesis: X3 /\ X4 = {}
thus  X3 /\ X4 = {} by A1, A2, A3, A6, A7, XBOOLE_1:3, XBOOLE_1:27; ::_thesis: verum
end;

registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc strict Colored-PT-net-like for Colored_PT_net_Str ;
existence
 ex b1 being Colored_Petri_net st
( b1 is strict & b1 is Colored-PT-net-like )
proof
set PLA = {0};
set a = the set ;
set TRA = { the set };
set TSA = [:{ the set },{0}:];
 [:{ the set },{0}:] c= [:{ the set },{0}:] ;
then reconsider TSA = [:{ the set },{0}:] as non empty Relation of { the set },{0} ;
set STA = [:{0},{ the set }:];
 [:{0},{ the set }:] c= [:{0},{ the set }:] ;
then reconsider STA = [:{0},{ the set }:] as non empty Relation of {0},{ the set } ;
set CS = { the set , the set , the set };
set fa = the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}));
set f = { the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}));
set CPNT = Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #);
A1: Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) is with_S-T_arc by PETRI:def_1;
 Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) is with_T-S_arc by PETRI:def_2;
then reconsider CPNT = Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) as Colored_Petri_net by A1;
take  CPNT ; ::_thesis: ( CPNT is strict & CPNT is Colored-PT-net-like )
A2: now__::_thesis:_for_t_being_transition_of_CPNT_st_t_in_dom_the_firing-rule_of_CPNT_holds_
ex_CS1_being_non_empty_Subset_of_the_ColoredSet_of_CPNT_ex_I_being_Subset_of_(*'_{t})_ex_O_being_Subset_of_({t}_*')_st_the_firing-rule_of_CPNT_._t_is_Function_of_(thin_cylinders_(CS1,I)),(thin_cylinders_(CS1,O))
 { the set , the set , the set } c= { the set , the set , the set } ;
then reconsider CS1 = { the set , the set , the set } as non empty Subset of the ColoredSet of CPNT ;
let t be transition of CPNT; ::_thesis: ( t in dom the firing-rule of CPNT implies ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) )
assume  t in dom the firing-rule of CPNT ; ::_thesis: ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O))
A3: t = the set by TARSKI:def_1;
A4: the set in { the set } by TARSKI:def_1;
A5: 0 in {0} by TARSKI:def_1;
then  [ the set ,0] in TSA by A4, ZFMISC_1:87;
then  0 in {t} *' by A3, PETRI:8;
then reconsider O = {0} as Subset of ({t} *') by ZFMISC_1:31;
 [0, the set ] in STA by A5, A4, ZFMISC_1:87;
then  0 in *' {t} by A3, PETRI:6;
then reconsider I = {0} as Subset of (*' {t}) by ZFMISC_1:31;
A6: the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0})) is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;
 ({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) . t = the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0})) by FUNCOP_1:7;
hence  ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) by A6; ::_thesis: verum
end;
A7: dom ({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) = { the set } by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_the_firing-rule_of_CPNT_holds_
x_in_the_carrier'_of_CPNT_\_(Outbds_CPNT)
reconsider a1 = the set as transition of CPNT by TARSKI:def_1;
let x be set ; ::_thesis: ( x in dom the firing-rule of CPNT implies x in the carrier' of CPNT \ (Outbds CPNT) )
 0 in {0} by TARSKI:def_1;
then  [a1,0] in TSA by ZFMISC_1:87;
then A8: not {a1} *' = {} by PETRI:8;
A9: not a1 in Outbds CPNT
proof
assume  a1 in Outbds CPNT ; ::_thesis: contradiction
then  ex x being transition of CPNT st
( a1 = x & x is outbound ) ;
hence  contradiction by A8, Def9; ::_thesis: verum
end;
assume  x in dom the firing-rule of CPNT ; ::_thesis: x in the carrier' of CPNT \ (Outbds CPNT)
then  x = the set by A7, TARSKI:def_1;
hence  x in the carrier' of CPNT \ (Outbds CPNT) by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
then  dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) by TARSKI:def_3;
hence  ( CPNT is strict & CPNT is Colored-PT-net-like ) by A2, Def11; ::_thesis: verum
end;
end;

definition
mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;
end;

begin

definition
let CPNT1, CPNT2 be Colored_Petri_net;
predCPNT1 misses CPNT2 means :Def12: :: PETRI_2:def 12
( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} );
symmetry
 for CPNT1, CPNT2 being Colored_Petri_net st the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} holds
( the carrier of CPNT2 /\ the carrier of CPNT1 = {} & the carrier' of CPNT2 /\ the carrier' of CPNT1 = {} ) ;
end;

:: deftheorem Def12 defines misses PETRI_2:def_12_:_
 for CPNT1, CPNT2 being Colored_Petri_net holds
( CPNT1 misses CPNT2 iff ( the carrier of CPNT1 /\ the carrier of CPNT2 = {} & the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} ) );

begin

definition
let CPNT1, CPNT2 be Colored_Petri_net;
mode connecting-mapping of CPNT1,CPNT2 ->  set  means :Def13: :: PETRI_2:def 13
 ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st it = [O12,O21];
correctness
existence
ex b1 being set ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st b1 = [O12,O21];
proof
set O12 = the Function of (Outbds CPNT1), the carrier of CPNT2;
set O21 = the Function of (Outbds CPNT2), the carrier of CPNT1;
set Z = [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1];
take  [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] ; ::_thesis: ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] = [O12,O21]
thus  ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st [ the Function of (Outbds CPNT1), the carrier of CPNT2, the Function of (Outbds CPNT2), the carrier of CPNT1] = [O12,O21] ; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines connecting-mapping PETRI_2:def_13_:_
 for CPNT1, CPNT2 being Colored_Petri_net
for b3 being set holds
( b3 is connecting-mapping of CPNT1,CPNT2 iff ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st b3 = [O12,O21] );

begin

definition
let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;
mode connecting-firing-rule of CPNT1,CPNT2,O ->  set  means :Def14: :: PETRI_2:def 14
 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)))) ) & it = [q12,q21] );
correctness
existence
ex b1 being set 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)))) ) & b1 = [q12,q21] );
proof
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[ 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 carrier of CPNT1, the ColoredSet of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the ColoredSet of CPNT1)))) & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in Outbds CPNT1 implies ex y being set 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 ; ::_thesis: ex y being set 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)))) ; ::_thesis: ( 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; ::_thesis: 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 set st x in Outbds CPNT1 holds
S2[x,q12 . x] from FUNCT_2:sch_1(A2);
A8: now__::_thesis:_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; ::_thesis: ( 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 ; ::_thesis: 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)))) ; ::_thesis: verum
end;
A9: for x being set st x in Outbds CPNT2 holds
ex y being set 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 set ; ::_thesis: ( x in Outbds CPNT2 implies ex y being set 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 ; ::_thesis: ex y being set 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)))) ; ::_thesis: ( 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; ::_thesis: 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 set st x in Outbds CPNT2 holds
S1[x,q21 . x] from FUNCT_2:sch_1(A9);
A15: now__::_thesis:_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; ::_thesis: ( 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 ; ::_thesis: 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)))) ; ::_thesis: verum
end;
take  [q12,q21] ; ::_thesis: 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; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines connecting-firing-rule PETRI_2:def_14_:_
 for CPNT1, CPNT2 being Colored-PT-net
for O being connecting-mapping of CPNT1,CPNT2
for b4 being set holds
( b4 is connecting-firing-rule of CPNT1,CPNT2,O iff 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)))) ) & b4 = [q12,q21] ) );

begin

definition
let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;
let q be connecting-firing-rule of CPNT1,CPNT2,O;
assume A1: CPNT1 misses CPNT2 ;
func synthesis (CPNT1,CPNT2,O,q) ->  strict Colored-PT-net means :: PETRI_2:def 15
 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)))) ) & q = [q12,q21] & the carrier of it = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of it = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of it = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of it = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of it = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of it = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 );
existence
 ex b1 being strict Colored-PT-net 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)))) ) & q = [q12,q21] & the carrier of b1 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b1 = the carrier' of CPNT1 \/ the carrier' 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 )
proof
reconsider CS12 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 as non empty finite set ;
reconsider T12 = the carrier' of CPNT1 \/ the carrier' of CPNT2 as non empty set ;
reconsider P12 = the carrier of CPNT1 \/ the carrier of CPNT2 as non empty set ;
A2: the carrier' of CPNT1 c= T12 by XBOOLE_1:7;
 the carrier 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:7;
A3: the carrier of CPNT2 c= P12 by XBOOLE_1:7;
 the carrier' 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:7;
set R1 = the firing-rule of CPNT1;
A4: the carrier' of CPNT2 c= T12 by XBOOLE_1:7;
 the carrier 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:7;
set R2 = the firing-rule of CPNT2;
A5: the carrier of CPNT1 c= P12 by XBOOLE_1:7;
 the carrier' 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:7;
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 carrier of CPNT2, O21 being Function of (Outbds CPNT2), the carrier 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 Def14;
A14: dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (dom q21) by A10, Def11;
 the carrier' of CPNT2 c= T12 by XBOOLE_1:7;
then A15: Outbds CPNT2 c= T12 by XBOOLE_1:1;
 the carrier' of CPNT1 c= T12 by XBOOLE_1:7;
then A16: Outbds CPNT1 c= T12 by XBOOLE_1:1;
A17: the carrier' of CPNT1 /\ the carrier' of CPNT2 = {} by A1, Def12;
A18: dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (dom q12) by A9, Def11;
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 carrier of CPNT1 c= P12 by XBOOLE_1:7;
then reconsider E32 = O21 as Relation of T12,P12 by A15, RELSET_1:7;
 the carrier of CPNT2 c= P12 by XBOOLE_1:7;
then reconsider E31 = O12 as Relation of T12,P12 by A16, RELSET_1:7;
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: Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) is with_S-T_arc by PETRI:def_1;
 Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) is with_T-S_arc by PETRI:def_2;
then reconsider CPNT12 = Colored_PT_net_Str(# P12,T12,ST12,TS12,CS12,((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) #) as Colored_Petri_net by A25;
A26: the carrier of CPNT1 c= the carrier of CPNT12 by XBOOLE_1:7;
A27: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
 the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
then A28: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT12 by A6, XBOOLE_1:1;
A29: the carrier of CPNT2 c= the carrier of CPNT12 by XBOOLE_1:7;
 the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
then A30: the T-S_Arcs of CPNT2 c= the T-S_Arcs of CPNT12 by A7, XBOOLE_1:1;
A31: the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12 by XBOOLE_1:7;
A32: now__::_thesis:_for_x_being_set_holds_
(_not_x_in_dom_(((_the_firing-rule_of_CPNT1_+*_the_firing-rule_of_CPNT2)_+*_q12)_+*_q21)_or_x_in_dom_the_firing-rule_of_CPNT1_or_x_in_dom_the_firing-rule_of_CPNT2_or_x_in_dom_q12_or_x_in_dom_q21_)
let x be set ; ::_thesis: ( not x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) or x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 )
assume  x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) ; ::_thesis: ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 )
then  ( x in dom (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) or x in dom q21 ) by FUNCT_4:12;
then  ( x in dom ( the firing-rule of CPNT1 +* the firing-rule of CPNT2) or x in dom q12 or x in dom q21 ) by FUNCT_4:12;
hence  ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 ) by FUNCT_4:12; ::_thesis: verum
end;
A33: for t being transition of CPNT12 st t in dom the firing-rule of CPNT12 holds
ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
proof
let t be transition of CPNT12; ::_thesis: ( t in dom the firing-rule of CPNT12 implies ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) )
assume A34: t in dom the firing-rule of CPNT12 ; ::_thesis: ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
now__::_thesis:_ex_CS_being_non_empty_Subset_of_the_ColoredSet_of_CPNT12_ex_I_being_Subset_of_(*'_{t})_ex_O_being_Subset_of_({t}_*')_st_the_firing-rule_of_CPNT12_._t_is_Function_of_(thin_cylinders_(CS,I)),(thin_cylinders_(CS,O))
percases ( 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 A32, A34;
supposeA35: t in dom the firing-rule of CPNT1 ; ::_thesis: ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
 dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (Outbds CPNT1) by Def11;
then reconsider t1 = t as transition of CPNT1 by A35, 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
A36: the firing-rule of CPNT1 . t1 is Function of (thin_cylinders (CS1,I1)),(thin_cylinders (CS1,O1)) by A35, Def11;
 *' {t1} c= *' {t} by A26, A27, A28, Th7;
then reconsider I = I1 as Subset of (*' {t}) by XBOOLE_1:1;
 the ColoredSet of CPNT1 c= the ColoredSet of CPNT12 by XBOOLE_1:7;
then reconsider CS = CS1 as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:1;
 {t1} *' c= {t} *' by A26, A27, A28, Th7;
then reconsider O = O1 as Subset of ({t} *') by XBOOLE_1:1;
 the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by A19, A24, A23, A21, A20, A22, A35, A36, Lm5;
hence  ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; ::_thesis: verum
end;
supposeA37: t in dom the firing-rule of CPNT2 ; ::_thesis: ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
 dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (Outbds CPNT2) by Def11;
then reconsider t1 = t as transition of CPNT2 by A37, 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
A38: the firing-rule of CPNT2 . t1 is Function of (thin_cylinders (CS1,I1)),(thin_cylinders (CS1,O1)) by A37, Def11;
 *' {t1} c= *' {t} by A29, A31, A30, Th7;
then reconsider I = I1 as Subset of (*' {t}) by XBOOLE_1:1;
 the ColoredSet of CPNT2 c= the ColoredSet of CPNT12 by XBOOLE_1:7;
then reconsider CS = CS1 as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:1;
 {t1} *' c= {t} *' by A29, A31, A30, Th7;
then reconsider O = O1 as Subset of ({t} *') by XBOOLE_1:1;
 the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by A19, A24, A23, A21, A20, A22, A37, A38, Lm5;
hence  ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; ::_thesis: verum
end;
supposeA39: t in dom q12 ; ::_thesis: ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . 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 A26, A27, A28, Th7;
reconsider CS = the ColoredSet of CPNT1 as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
 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} *' )
A40: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
assume A41: x in Im (O12,t1) ; ::_thesis: x in {t} *'
then reconsider s = x as place of CPNT2 ;
A42: [t1,s] in O12 by A41, RELSET_2:9;
 O12 c= E31 \/ E32 by XBOOLE_1:7;
then  O12 c= the T-S_Arcs of CPNT12 by A40, XBOOLE_1:1;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A42;
A43: the carrier of CPNT2 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A44: f = [t,s] ;
A45: t in {t} by TARSKI:def_1;
 s in the carrier of CPNT2 ;
hence  x in {t} *' by A43, A45, A44; ::_thesis: 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, A39;
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 CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by A19, A24, A23, A21, A20, A22, A39, Lm5;
hence  ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; ::_thesis: verum
end;
supposeA46: t in dom q21 ; ::_thesis: ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . 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 A29, A31, A30, Th7;
reconsider CS = the ColoredSet of CPNT2 as non empty Subset of the ColoredSet of CPNT12 by XBOOLE_1:7;
 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} *' )
A47: O21 c= E31 \/ E32 by XBOOLE_1:7;
assume A48: x in Im (O21,t1) ; ::_thesis: x in {t} *'
then reconsider s = x as place of CPNT1 ;
A49: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
 [t1,s] in O21 by A48, RELSET_2:9;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A47, A49, TARSKI:def_3;
A50: the carrier of CPNT1 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A51: f = [t,s] ;
A52: t in {t} by TARSKI:def_1;
 s in the carrier of CPNT1 ;
hence  x in {t} *' by A50, A52, A51; ::_thesis: 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, A46;
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 CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) by A19, A24, A23, A21, A20, A22, A46, Lm5;
hence  ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; ::_thesis: verum
end;
end;
end;
hence  ex CS being non empty Subset of the ColoredSet of CPNT12 ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT12 . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; ::_thesis: verum
end;
A53: TS12 = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 by XBOOLE_1:4;
A54: now__::_thesis:_for_x_being_set_st_x_in_dom_(((_the_firing-rule_of_CPNT1_+*_the_firing-rule_of_CPNT2)_+*_q12)_+*_q21)_holds_
x_in_the_carrier'_of_CPNT1_\/_the_carrier'_of_CPNT2
let x be set ; ::_thesis: ( x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) implies x in the carrier' of CPNT1 \/ the carrier' of CPNT2 )
 dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (Outbds CPNT1) by Def11;
then A55: dom the firing-rule of CPNT1 c= the carrier' of CPNT1 by XBOOLE_1:1;
 dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (Outbds CPNT2) by Def11;
then A56: dom the firing-rule of CPNT2 c= the carrier' of CPNT2 by XBOOLE_1:1;
assume  x in dom ((( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21) ; ::_thesis: x in the carrier' of CPNT1 \/ the carrier' of CPNT2
then  ( x in dom the firing-rule of CPNT1 or x in dom the firing-rule of CPNT2 or x in dom q12 or x in dom q21 ) by A32;
hence  x in the carrier' of CPNT1 \/ the carrier' of CPNT2 by A9, A10, A55, A56, XBOOLE_0:def_3; ::_thesis: verum
end;
then A57: dom the firing-rule of CPNT12 c= the carrier' of CPNT12 by TARSKI:def_3;
 dom the firing-rule of CPNT12 c= the carrier' of CPNT12 \ (Outbds CPNT12)
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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom the firing-rule of CPNT12 or x in the carrier' of CPNT12 \ (Outbds CPNT12) )
assume A58: x in dom the firing-rule of CPNT12 ; ::_thesis: x in the carrier' of CPNT12 \ (Outbds CPNT12)
then reconsider t = x as transition of CPNT12 by A54;
now__::_thesis:_not_x_in_Outbds_CPNT12
percases ( 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 A32, A58;
supposeA59: t in dom the firing-rule of CPNT1 ; ::_thesis: not x in Outbds CPNT12
A60: dom the firing-rule of CPNT1 c= the carrier' of CPNT1 \ (Outbds CPNT1) by Def11;
then reconsider t1 = t as transition of CPNT1 by A59, XBOOLE_0:def_5;
 not t in Outbds CPNT1 by A59, A60, XBOOLE_0:def_5;
then  not t1 is outbound ;
then  {t1} *' <> {} by Def9;
then A61: ex g being set st g in {t1} *' by XBOOLE_0:def_1;
 {t1} *' c= {t} *' by A26, A27, A28, Th7;
then  for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by A61, Def9;
hence  not x in Outbds CPNT12 ; ::_thesis: verum
end;
supposeA62: t in dom the firing-rule of CPNT2 ; ::_thesis: not x in Outbds CPNT12
A63: dom the firing-rule of CPNT2 c= the carrier' of CPNT2 \ (Outbds CPNT2) by Def11;
then reconsider t1 = t as transition of CPNT2 by A62, XBOOLE_0:def_5;
 not t in Outbds CPNT2 by A62, A63, XBOOLE_0:def_5;
then  not t1 is outbound ;
then  {t1} *' <> {} by Def9;
then A64: ex g being set st g in {t1} *' by XBOOLE_0:def_1;
 {t1} *' c= {t} *' by A29, A31, A30, Th7;
then  for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by A64, Def9;
hence  not x in Outbds CPNT12 ; ::_thesis: verum
end;
suppose t in dom q12 ; ::_thesis: not x in Outbds CPNT12
then  t in dom O12 by A9, FUNCT_2:def_1;
then consider s being set  such that
A65: [t,s] in O12 by XTUPLE_0:def_12;
reconsider s = s as place of CPNT2 by A65, ZFMISC_1:87;
A66: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
 O12 c= E31 \/ E32 by XBOOLE_1:7;
then  O12 c= the T-S_Arcs of CPNT12 by A66, XBOOLE_1:1;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A65;
A67: the carrier of CPNT2 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A68: f = [t,s] ;
A69: t in {t} by TARSKI:def_1;
 s in the carrier of CPNT2 ;
then  s in {t} *' by A67, A69, A68;
then  for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by Def9;
hence  not x in Outbds CPNT12 ; ::_thesis: verum
end;
suppose t in dom q21 ; ::_thesis: not x in Outbds CPNT12
then  t in dom O21 by A10, FUNCT_2:def_1;
then consider s being set  such that
A70: [t,s] in O21 by XTUPLE_0:def_12;
reconsider s = s as place of CPNT1 by A70, ZFMISC_1:87;
A71: E31 \/ E32 c= the T-S_Arcs of CPNT12 by XBOOLE_1:7;
 O21 c= E31 \/ E32 by XBOOLE_1:7;
then  O21 c= the T-S_Arcs of CPNT12 by A71, XBOOLE_1:1;
then reconsider f = [t,s] as T-S_arc of CPNT12 by A70;
A72: the carrier of CPNT1 c= the carrier of CPNT1 \/ the carrier of CPNT2 by XBOOLE_1:7;
A73: f = [t,s] ;
A74: t in {t} by TARSKI:def_1;
 s in the carrier of CPNT1 ;
then  s in {t} *' by A72, A74, A73;
then  for w being transition of CPNT12 holds
( not t = w or not w is outbound ) by Def9;
hence  not x in Outbds CPNT12 ; ::_thesis: verum
end;
end;
end;
hence  x in the carrier' of CPNT12 \ (Outbds CPNT12) by A57, A58, XBOOLE_0:def_5; ::_thesis: verum
end;
then  CPNT12 is Colored-PT-net-like by A33, Def11;
hence  ex b1 being strict Colored-PT-net 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)))) ) & q = [q12,q21] & the carrier of b1 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b1 = the carrier' of CPNT1 \/ the carrier' 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, A53; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Colored-PT-net st 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)))) ) & q = [q12,q21] & the carrier of b1 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b1 = the carrier' of CPNT1 \/ the carrier' 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 ) & 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)))) ) & q = [q12,q21] & the carrier of b2 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b2 = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b2 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b2 = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b2 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b2 = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) holds
b1 = b2
proof
let CA, CB be strict Colored-PT-net; ::_thesis: ( 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)))) ) & q = [q12,q21] & the carrier of CA = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* 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)))) ) & q = [q12,q21] & the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) implies CA = CB )
assume  ex q12A, q21A being Function ex O12A being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21A being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12A,O21A] & dom q12A = Outbds CPNT1 & dom q21A = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12A . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12A,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21A . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21A,t02)))) ) & q = [q12A,q21A] & the carrier of CA = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A & the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12A) +* q21A ) ; ::_thesis: ( for q12, q21 being Function
for O12 being Function of (Outbds CPNT1), the carrier of CPNT2
for O21 being Function of (Outbds CPNT2), the carrier of CPNT1 holds
( not O = [O12,O21] or not dom q12 = Outbds CPNT1 or not dom q21 = Outbds CPNT2 or ex t01 being transition of CPNT1 st
( t01 is outbound & q12 . t01 is not Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) or ex t02 being transition of CPNT2 st
( t02 is outbound & q21 . t02 is not Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21,t02)))) ) or not q = [q12,q21] or not the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 or not the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 or not the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 or not the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 or not the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 or not the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) or CA = CB )
then consider q12A, q21A being Function, O12A being Function of (Outbds CPNT1), the carrier of CPNT2, O21A being Function of (Outbds CPNT2), the carrier of CPNT1 such that
A75: O = [O12A,O21A] and
 dom q12A = Outbds CPNT1 and
 dom q21A = Outbds CPNT2 and
 for t01 being transition of CPNT1 st t01 is outbound holds
q12A . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12A,t01)))) and
 for t02 being transition of CPNT2 st t02 is outbound holds
q21A . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21A,t02)))) and
A76: q = [q12A,q21A] and
A77: the carrier of CA = the carrier of CPNT1 \/ the carrier of CPNT2 and
A78: the carrier' of CA = the carrier' of CPNT1 \/ the carrier' of CPNT2 and
A79: the S-T_Arcs of CA = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 and
A80: the T-S_Arcs of CA = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A and
A81: the ColoredSet of CA = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 and
A82: the firing-rule of CA = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12A) +* q21A ;
assume  ex q12B, q21B being Function ex O12B being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21B being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12B,O21B] & dom q12B = Outbds CPNT1 & dom q21B = Outbds CPNT2 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12B . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12B,t01)))) ) & ( for t02 being transition of CPNT2 st t02 is outbound holds
q21B . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21B,t02)))) ) & q = [q12B,q21B] & the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B & the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12B) +* q21B ) ; ::_thesis: CA = CB
then consider q12B, q21B being Function, O12B being Function of (Outbds CPNT1), the carrier of CPNT2, O21B being Function of (Outbds CPNT2), the carrier of CPNT1 such that
A83: O = [O12B,O21B] and
 dom q12B = Outbds CPNT1 and
 dom q21B = Outbds CPNT2 and
 for t01 being transition of CPNT1 st t01 is outbound holds
q12B . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12B,t01)))) and
 for t02 being transition of CPNT2 st t02 is outbound holds
q21B . t02 is Function of (thin_cylinders ( the ColoredSet of CPNT2,(*' {t02}))),(thin_cylinders ( the ColoredSet of CPNT2,(Im (O21B,t02)))) and
A84: q = [q12B,q21B] and
A85: the carrier of CB = the carrier of CPNT1 \/ the carrier of CPNT2 and
A86: the carrier' of CB = the carrier' of CPNT1 \/ the carrier' of CPNT2 and
A87: the S-T_Arcs of CB = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 and
A88: the T-S_Arcs of CB = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B and
A89: the ColoredSet of CB = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 and
A90: the firing-rule of CB = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12B) +* q21B ;
A91: q21A = q21B by A76, A84, XTUPLE_0:1;
A92: O12A = O12B by A75, A83, XTUPLE_0:1;
 q12A = q12B by A76, A84, XTUPLE_0:1;
hence  CA = CB by A75, A77, A78, A79, A80, A81, A82, A83, A85, A86, A87, A88, A89, A90, A91, A92, XTUPLE_0:1; ::_thesis: verum
end;
end;

:: deftheorem  defines synthesis PETRI_2:def_15_:_
 for CPNT1, CPNT2 being Colored-PT-net
for O being connecting-mapping of CPNT1,CPNT2
for q being connecting-firing-rule of CPNT1,CPNT2,O st CPNT1 misses CPNT2 holds
for b5 being strict Colored-PT-net holds
( b5 = synthesis (CPNT1,CPNT2,O,q) iff 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)))) ) & q = [q12,q21] & the carrier of b5 = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b5 = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b5 = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b5 = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b5 = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b5 = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) );