:: 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 ) );