petri_2.miz



    begin

    definition

      let A be non empty set, B be set;

      let Bo be set, yo be Function of Bo, A;

      assume

       A1: Bo c= B;

      :: PETRI_2:def1

      func cylinder0 (A,B,Bo,yo) -> non empty Subset of ( Funcs (B,A)) equals

      : Def1: { y where y be Function of B, A : (y | Bo) = yo };

      correctness

      proof

        set D = { y where y be Function of B, A : (y | Bo) = yo };

         A2:

        now

          per cases ;

            suppose

             A3: Bo = {} ;

            set f = the Function of B, A;

            (f | {} ) = {}

            .= yo by A3;

            then f in D by A3;

            hence D is non empty;

          end;

            suppose Bo <> {} ;

            then

            consider b0 be object 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 f) 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 f) = (( 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;

            then (( rng (B --> (yo . b0))) \/ ( rng yo)) c= A by A7, XBOOLE_1: 8;

            then

            reconsider f 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 D;

            hence D is non empty;

          end;

        end;

        now

          let z be object;

          assume z in D;

          then ex y be Function of B, A st z = y & (y | Bo) = yo;

          hence z in ( Funcs (B,A)) by FUNCT_2: 8;

        end;

        hence thesis by A2, TARSKI:def 3;

      end;

    end

    definition

      let A be non empty set, B be set;

      :: PETRI_2:def2

      mode thin_cylinder of A,B -> non empty Subset of ( Funcs (B,A)) means

      : Def2: ex Bo be Subset of B, yo be Function of Bo, A st Bo is finite & it = ( cylinder0 (A,B,Bo,yo));

      existence

      proof

        set Bo = {} ;

        set yo = the Function of Bo, A;

        take ( cylinder0 (A,B,Bo,yo));

        Bo is Subset of B by XBOOLE_1: 2;

        hence thesis;

      end;

    end

    theorem :: PETRI_2:1

    

     Th1: for A be non empty set, B be set, D be thin_cylinder of A, B holds ex Bo be Subset of B, yo be Function of Bo, A st Bo is finite & D = { y where y be Function of B, A : (y | Bo) = yo }

    proof

      let A be non empty set, B be set, D be thin_cylinder of A, B;

      consider Bo be Subset of B, yo be Function of Bo, A such that

       A1: Bo is finite and

       A2: D = ( cylinder0 (A,B,Bo,yo)) by Def2;

      D = { y where y be Function of B, A : (y | Bo) = yo } by A2, Def1;

      hence thesis by A1;

    end;

    theorem :: PETRI_2:2

    for A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1, B st A1 c= A2 holds ex D2 be thin_cylinder of A2, B st D1 c= D2

    proof

      let A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1, B;

      consider Bo be Subset of B, yo1 be Function of Bo, A1 such that

       A1: Bo is finite and

       A2: D1 = { y where y be Function of B, A1 : (y | Bo) = yo1 } by Th1;

      assume

       A3: A1 c= A2;

      then

      reconsider yo2 = yo1 as Function of Bo, A2 by FUNCT_2: 7;

      set D2 = { y where y be Function of B, A2 : (y | Bo) = yo2 };

       A4:

      now

        let x be object;

        assume x in D1;

        then

        consider y1 be 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 D2 by A5;

      end;

      D2 = ( cylinder0 (A2,B,Bo,yo2)) by Def1;

      then

      reconsider D2 as thin_cylinder of A2, B by A1, Def2;

      take D2;

      thus thesis by A4;

    end;

    definition

      let A be non empty set, B be set;

      :: PETRI_2:def3

      func thin_cylinders (A,B) -> non empty Subset-Family of ( Funcs (B,A)) equals { D where D be Subset of ( Funcs (B,A)) : D is thin_cylinder of A, B };

      correctness

      proof

        set F = the thin_cylinder of A, B;

         A1:

        now

          let z be object;

          assume z in { D where D be Subset of ( Funcs (B,A)) : D is thin_cylinder of A, B };

          then ex D be Subset of ( Funcs (B,A)) st z = D & D is thin_cylinder of A, B;

          hence z in ( bool ( Funcs (B,A)));

        end;

        F in { D where D be Subset of ( Funcs (B,A)) : D is thin_cylinder of A, B };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    

     Lm1: for A be non empty set, B,C be set st B c= C holds ( thin_cylinders (A,B)) c= ( bool ( PFuncs (C,A)))

    proof

      let A be non empty set, B,C be set;

      assume B c= C;

      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;

      then

       A2: ( bool ( Funcs (B,A))) c= ( bool ( PFuncs (C,A))) by ZFMISC_1: 67;

      let x be object;

      assume x in ( thin_cylinders (A,B));

      then

      consider D be Subset of ( Funcs (B,A)) such that

       A3: x = D and D is thin_cylinder of A, B;

      thus thesis by A3, A2;

    end;

    

     Lm2: for A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A st not Bo2 c= Bo1 holds ex f be Function of B, A st (f | Bo1) = yo1 & (f | Bo2) <> yo2

    proof

      let A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A;

      defpred C[ object] means $1 in Bo1;

      deffunc F( object) = (yo1 . $1);

      assume not Bo2 c= Bo1;

      then

      consider x0 be object such that

       A1: x0 in Bo2 and

       A2: not x0 in Bo1;

      

       A3: x0 in ( dom yo2) by A1, FUNCT_2:def 1;

      ex y0 be set st y0 in A & y0 <> (yo2 . x0)

      proof

        consider x,y be object such that

         A4: x in A and

         A5: y in A and

         A6: x <> y by ZFMISC_1:def 10;

        per cases ;

          suppose

           A7: (yo2 . x0) = x;

          take y;

          thus thesis by A5, A6, A7;

        end;

          suppose

           A8: (yo2 . x0) <> x;

          take x;

          thus thesis by A4, A8;

        end;

      end;

      then

      consider y0 be set such that

       A9: y0 in A and

       A10: y0 <> (yo2 . x0);

      deffunc G( object) = y0;

      

       A11: for x be object st x in B holds ( C[x] implies F(x) in A) & ( not C[x] implies G(x) in A) by A9, FUNCT_2: 5;

      consider f be Function of B, A such that

       A12: for x be object st x in B holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A11);

       A13:

      now

        let z be object;

        assume z in ( dom yo1);

        then z in Bo1;

        hence (yo1 . z) = (f . z) by A12;

      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 thesis by A14;

    end;

    

     Lm3: for A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A st Bo1 <> Bo2 & Bo2 c= Bo1 holds ex f be Function of B, A st (f | Bo2) = yo2 & (f | Bo1) <> yo1

    proof

      let A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A;

      assume that

       A1: Bo1 <> Bo2 and

       A2: Bo2 c= Bo1;

      Bo2 c< Bo1 by A1, A2, XBOOLE_0:def 8;

      then

      consider x0 be object 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 F( object) = (yo2 . $1);

      defpred C[ object] means $1 in Bo2;

      ex y0 be set st y0 in A & y0 <> (yo1 . x0)

      proof

        consider x,y be object such that

         A6: x in A and

         A7: y in A and

         A8: x <> y by ZFMISC_1:def 10;

        per cases ;

          suppose

           A9: (yo1 . x0) = x;

          take y;

          thus thesis by A7, A8, A9;

        end;

          suppose

           A10: (yo1 . x0) <> x;

          take x;

          thus thesis by A6, A10;

        end;

      end;

      then

      consider y0 be set such that

       A11: y0 in A and

       A12: y0 <> (yo1 . x0);

      deffunc G( object) = y0;

      

       A13: for x be object st x in B holds ( C[x] implies F(x) in A) & ( not C[x] implies G(x) in A) by A11, FUNCT_2: 5;

      consider f be Function of B, A such that

       A14: for x be object st x in B holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A13);

       A15:

      now

        let z be object;

        assume z in ( dom yo2);

        then z in Bo2;

        hence (yo2 . z) = (f . z) by A14;

      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 thesis by A16;

    end;

    

     Lm4: for A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A st Bo1 <> Bo2 holds { y where y be Function of B, A : (y | Bo1) = yo1 } <> { y where y be Function of B, A : (y | Bo2) = yo2 }

    proof

      let A be non trivial set, B be set, Bo1,Bo2 be Subset of B, yo1 be Function of Bo1, A, yo2 be Function of Bo2, A;

      assume

       A1: Bo1 <> Bo2;

      per cases ;

        suppose not Bo2 c= Bo1;

        then

        consider f be Function of B, A such that

         A2: (f | Bo1) = yo1 and

         A3: (f | Bo2) <> yo2 by Lm2;

         not f in { y where y be Function of B, A : (y | Bo2) = yo2 }

        proof

          assume f in { y where y be Function of B, A : (y | Bo2) = yo2 };

          then ex y be Function of B, A st f = y & (y | Bo2) = yo2;

          hence contradiction by A3;

        end;

        hence thesis by A2;

      end;

        suppose Bo2 c= Bo1;

        then

        consider f be Function of B, A such that

         A4: (f | Bo2) = yo2 and

         A5: (f | Bo1) <> yo1 by A1, Lm3;

         not f in { y where y be Function of B, A : (y | Bo1) = yo1 }

        proof

          assume f in { y where y be Function of B, A : (y | Bo1) = yo1 };

          then ex y be Function of B, A st f = y & (y | Bo1) = yo1;

          hence contradiction by A5;

        end;

        hence thesis by A4;

      end;

    end;

    theorem :: PETRI_2:3

    

     Th3: for A be non trivial set, B be set, Bo1 be set, yo1 be Function of Bo1, A, Bo2 be set, yo2 be 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, B be set, Bo1 be set, yo1 be Function of Bo1, A, Bo2 be set, yo2 be Function of Bo2, A;

      assume that

       A1: Bo1 c= B and

       A2: Bo2 c= B and

       A3: ( cylinder0 (A,B,Bo1,yo1)) = ( cylinder0 (A,B,Bo2,yo2));

      

       A4: { y where y be Function of B, A : (y | Bo1) = yo1 } = ( cylinder0 (A,B,Bo1,yo1)) by A1, Def1;

      then

      consider y0 be object such that

       A5: y0 in { y where y be Function of B, A : (y | Bo1) = yo1 } by XBOOLE_0:def 1;

      

       A6: ex y be Function of B, A st y0 = y & (y | Bo1) = yo1 by A5;

      

       A7: { y where y be Function of B, A : (y | Bo2) = yo2 } = ( cylinder0 (A,B,Bo2,yo2)) by A2, Def1;

      hence Bo1 = Bo2 by A1, A2, A3, A4, Lm4;

      ex w be Function of B, A st y0 = w & (w | Bo2) = yo2 by A3, A4, A7, A5;

      hence thesis by A1, A2, A3, A4, A7, A6, Lm4;

    end;

    theorem :: PETRI_2:4

    

     Th4: for A1,A2 be non empty set, B1,B2 be set st A1 c= A2 & B1 c= B2 holds ex F be Function of ( thin_cylinders (A1,B1)), ( thin_cylinders (A2,B2)) st for x be set st x in ( thin_cylinders (A1,B1)) holds ex Bo be Subset of B1, yo1 be Function of Bo, A1, yo2 be 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, B1,B2 be set;

      assume that

       A1: A1 c= A2 and

       A2: B1 c= B2;

      defpred P[ object, object] means ex Bo be Subset of B1, yo1 be Function of Bo, A1, yo2 be Function of Bo, A2 st Bo is finite & yo1 = yo2 & $1 = ( cylinder0 (A1,B1,Bo,yo1)) & $2 = ( cylinder0 (A2,B2,Bo,yo2));

       A3:

      now

        let x be object;

        assume x in ( thin_cylinders (A1,B1));

        then ex D be 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 be Subset of B1, yo1 be 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;

        then

         A6: D2 is thin_cylinder of A2, B2 by A4, Def2;

        reconsider D2 as object;

        take D2;

        thus D2 in ( thin_cylinders (A2,B2)) & P[x, D2] by A4, A5, A6;

      end;

      consider F be Function of ( thin_cylinders (A1,B1)), ( thin_cylinders (A2,B2)) such that

       A7: for x be object st x in ( thin_cylinders (A1,B1)) holds P[x, (F . x)] from FUNCT_2:sch 1( A3);

      take F;

      thus thesis by A7;

    end;

    theorem :: PETRI_2:5

    

     Th5: for A1,A2 be non empty set, B1,B2 be set holds ex G be Function of ( thin_cylinders (A2,B2)), ( thin_cylinders (A1,B1)) st for x be set st x in ( thin_cylinders (A2,B2)) holds ex Bo2 be Subset of B2, Bo1 be Subset of B1, yo1 be Function of Bo1, A1, yo2 be 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, B1,B2 be set;

      defpred P[ object, object] means ex Bo2 be Subset of B2, Bo1 be Subset of B1, yo1 be Function of Bo1, A1, yo2 be 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

        let x be object;

        assume x in ( thin_cylinders (A2,B2));

        then ex D be 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 be Subset of B2, yo2 be 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: Bo1 c= (B1 /\ Bo2) by XBOOLE_1: 17;

        set yo1 = (yo2 | Bo1);

        (B1 /\ Bo2) c= Bo2 by XBOOLE_1: 17;

        then Bo1 c= Bo2 by A4;

        then

         A5: yo1 is Function of Bo1, A2 by FUNCT_2: 32;

        

         A6: ( rng yo1) = (yo2 .: Bo1) by RELAT_1: 115;

        

         A7: (yo2 .: Bo1) c= (yo2 .: (yo2 " A1)) by RELAT_1: 123, XBOOLE_1: 17;

        (yo2 .: (yo2 " A1)) c= A1 by FUNCT_1: 75;

        then (yo2 .: Bo1) c= A1 by A7;

        then

        reconsider yo1 as Function of Bo1, A1 by A5, A6, FUNCT_2: 6;

        set D1 = ( cylinder0 (A1,B1,Bo1,yo1));

        (B1 /\ Bo2) c= B1 by XBOOLE_1: 17;

        then

         A8: Bo1 c= B1 by A4;

        then

         A9: D1 is thin_cylinder of A1, B1 by A2, Def2;

        reconsider D1 as object;

        take D1;

        thus D1 in ( thin_cylinders (A1,B1)) & P[x, D1] by A2, A3, A8, A9;

      end;

      consider G be Function of ( thin_cylinders (A2,B2)), ( thin_cylinders (A1,B1)) such that

       A10: for x be object st x in ( thin_cylinders (A2,B2)) holds P[x, (G . x)] from FUNCT_2:sch 1( A1);

      take G;

      thus thesis by A10;

    end;

    definition

      let A1,A2 be non trivial set, B1,B2 be set;

      assume that

       A1: A1 c= A2 and

       A2: B1 c= B2;

      :: PETRI_2:def4

      func Extcylinders (A1,B1,A2,B2) -> Function of ( thin_cylinders (A1,B1)), ( thin_cylinders (A2,B2)) means for x be set st x in ( thin_cylinders (A1,B1)) holds ex Bo be Subset of B1, yo1 be Function of Bo, A1, yo2 be Function of Bo, A2 st Bo is finite & yo1 = yo2 & x = ( cylinder0 (A1,B1,Bo,yo1)) & (it . x) = ( cylinder0 (A2,B2,Bo,yo2));

      existence by A1, A2, Th4;

      uniqueness

      proof

        let F1,F2 be Function of ( thin_cylinders (A1,B1)), ( thin_cylinders (A2,B2));

        assume

         A3: for x be set st x in ( thin_cylinders (A1,B1)) holds ex Bo be Subset of B1, yo1 be Function of Bo, A1, yo2 be Function of Bo, A2 st Bo is finite & yo1 = yo2 & x = ( cylinder0 (A1,B1,Bo,yo1)) & (F1 . x) = ( cylinder0 (A2,B2,Bo,yo2));

        assume

         A4: for x be set st x in ( thin_cylinders (A1,B1)) holds ex Bo be Subset of B1, yo1 be Function of Bo, A1, yo2 be Function of Bo, A2 st Bo is finite & yo1 = yo2 & x = ( cylinder0 (A1,B1,Bo,yo1)) & (F2 . x) = ( cylinder0 (A2,B2,Bo,yo2));

        now

          let x be object;

          assume

           A5: x in ( thin_cylinders (A1,B1));

          then

          consider Bo1 be Subset of B1, yo11 be Function of Bo1, A1, yo21 be 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 be Subset of B1, yo12 be Function of Bo2, A1, yo22 be 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;

        end;

        hence F1 = F2 by FUNCT_2: 12;

      end;

    end

    definition

      let A1 be non empty set, A2 be non trivial set, B1,B2 be set;

      :: PETRI_2:def5

      func Ristcylinders (A1,B1,A2,B2) -> Function of ( thin_cylinders (A2,B2)), ( thin_cylinders (A1,B1)) means for x be set st x in ( thin_cylinders (A2,B2)) holds ex Bo2 be Subset of B2, Bo1 be Subset of B1, yo1 be Function of Bo1, A1, yo2 be 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 by Th5;

      uniqueness

      proof

        let F1,F2 be Function of ( thin_cylinders (A2,B2)), ( thin_cylinders (A1,B1));

        assume

         A1: for x be set st x in ( thin_cylinders (A2,B2)) holds ex Bo21 be Subset of B2, Bo11 be Subset of B1, yo11 be Function of Bo11, A1, yo21 be 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));

        assume

         A2: for x be set st x in ( thin_cylinders (A2,B2)) holds ex Bo22 be Subset of B2, Bo12 be Subset of B1, yo12 be Function of Bo12, A1, yo22 be 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));

        now

          let x be object;

          assume

           A3: x in ( thin_cylinders (A2,B2));

          then

          consider Bo21 be Subset of B2, Bo11 be Subset of B1, yo11 be Function of Bo11, A1, yo21 be 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 be Subset of B2, Bo12 be Subset of B1, yo12 be Function of Bo12, A1, yo22 be 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;

        end;

        hence F1 = F2 by FUNCT_2: 12;

      end;

    end

    definition

      let A be non trivial set, B be set;

      let D be thin_cylinder of A, B;

      :: PETRI_2:def6

      func loc (D) -> finite Subset of B means ex Bo be Subset of B, yo be Function of Bo, A st Bo is finite & D = { y where y be Function of B, A : (y | Bo) = yo } & it = Bo;

      existence

      proof

        ex Bo be Subset of B, yo be Function of Bo, A st Bo is finite & D = { y where y be Function of B, A : (y | Bo) = yo } by Th1;

        hence thesis;

      end;

      uniqueness by Lm4;

    end

    begin

    definition

      let A1,A2 be non trivial set, B1,B2 be set;

      let C1,C2 be non trivial set, D1,D2 be set;

      let F be Function of ( thin_cylinders (A1,B1)), ( thin_cylinders (C1,D1));

      :: PETRI_2:def7

      func CylinderFunc (A1,B1,A2,B2,C1,D1,C2,D2,F) -> Function of ( thin_cylinders (A2,B2)), ( thin_cylinders (C2,D2)) equals ((( Extcylinders (C1,D1,C2,D2)) * F) * ( Ristcylinders (A1,B1,A2,B2)));

      correctness ;

    end

    definition

      struct ( PT_net_Str) Colored_PT_net_Str (# the carrier, carrier' -> set,

the S-T_Arcs -> Relation of the carrier, the carrier',

the T-S_Arcs -> Relation of the carrier', the carrier,

the ColoredSet -> non empty finite set,

the firing-rule -> Function #)

       attr strict strict;

    end

    definition

      :: PETRI_2:def8

      func TrivialColoredPetriNet -> Colored_PT_net_Str equals Colored_PT_net_Str (# { {} }, { {} }, ( [#] ( { {} }, { {} })), ( [#] ( { {} }, { {} })), { {} }, {} #);

      coherence ;

    end

    registration

      cluster TrivialColoredPetriNet -> with_S-T_arc with_T-S_arc non empty non void;

      coherence ;

    end

    registration

      cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str;

      existence

      proof

        take TrivialColoredPetriNet ;

        thus thesis;

      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;

      :: PETRI_2:def9

      attr t0 is outbound means ( {t0} *' ) = {} ;

    end

    definition

      let CPNT1 be Colored_Petri_net;

      :: PETRI_2:def10

      func Outbds (CPNT1) -> Subset of the carrier' of CPNT1 equals { x where x be transition of CPNT1 : x is outbound };

      coherence

      proof

        { x where x be transition of CPNT1 : x is outbound } c= the carrier' of CPNT1

        proof

          let z be object;

          assume z in { x where x be transition of CPNT1 : x is outbound };

          then ex x be transition of CPNT1 st z = x & x is outbound;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let CPNT be Colored_Petri_net;

      :: PETRI_2:def11

      attr CPNT is Colored-PT-net-like means

      : Def11: ( dom the firing-rule of CPNT) c= (the carrier' of CPNT \ ( Outbds CPNT)) & for t be transition of CPNT st t in ( dom the firing-rule of CPNT) holds ex CS be non empty Subset of the ColoredSet of CPNT, I be Subset of ( *' {t}), O be Subset of ( {t} *' ) st (the firing-rule of CPNT . t) is Function of ( thin_cylinders (CS,I)), ( thin_cylinders (CS,O));

    end

    theorem :: PETRI_2:6

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

    theorem :: PETRI_2:7

    

     Th7: for CPNT1,CPNT2 be Colored_Petri_net, t1 be transition of CPNT1, t2 be 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, t1 be transition of CPNT1, t2 be transition of CPNT2;

      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;

      thus ( *' {t1}) c= ( *' {t2})

      proof

        let x be object;

        assume

         A5: x in ( *' {t1});

        then

         A6: x is place of CPNT2 by A1;

        ex s be place of CPNT1 st x = s & ex f be S-T_arc of CPNT1, w be transition of CPNT1 st w in {t1} & f = [s, w] by A5;

        then

        consider f be S-T_arc of CPNT1, w be 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;

        hence thesis by A7, A8, A6;

      end;

      let x be object;

      assume

       A9: x in ( {t1} *' );

      then

       A10: x is place of CPNT2 by A1;

      ex s be place of CPNT1 st x = s & ex f be T-S_arc of CPNT1, w be transition of CPNT1 st w in {t1} & f = [w, s] by A9;

      then

      consider f be T-S_arc of CPNT1, w be 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;

      hence thesis by A11, A12, A10;

    end;

    

     Lm5: for f1,f2,f3,f4,g be 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 be set st x in ( dom f1) holds (g . x) = (f1 . x)) & (for x be set st x in ( dom f2) holds (g . x) = (f2 . x)) & (for x be set st x in ( dom f3) holds (g . x) = (f3 . x)) & for x be set st x in ( dom f4) holds (g . x) = (f4 . x)

    proof

      let f1,f2,f3,f4,g be Function;

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

      set f123 = ((f1 +* f2) +* f3);

      set f12 = (f1 +* f2);

      thus for x be set st x in ( dom f1) holds (g . x) = (f1 . x)

      proof

        let x be set;

        assume

         A8: x in ( dom f1);

        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) = (f123 . x) by A7, FUNCT_4: 11

        .= (f12 . x) by A9, FUNCT_4: 11

        .= (f1 . x) by A10, FUNCT_4: 11;

      end;

      thus for x be set st x in ( dom f2) holds (g . x) = (f2 . x)

      proof

        let x be set;

        assume

         A11: x in ( dom f2);

        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) = (f123 . x) by A7, FUNCT_4: 11

        .= (f12 . x) by A12, FUNCT_4: 11

        .= (f2 . x) by A11, FUNCT_4: 13;

      end;

      thus for x be set st x in ( dom f3) holds (g . x) = (f3 . x)

      proof

        let x be set;

        assume

         A13: x in ( dom f3);

        then not x in ( dom f4) by A6, XBOOLE_0:def 4;

        

        hence (g . x) = (f123 . x) by A7, FUNCT_4: 11

        .= (f3 . x) by A13, FUNCT_4: 13;

      end;

      thus thesis by A7, FUNCT_4: 13;

    end;

    

     Lm6: for A,B,C,D,X1,X2,X3,X4 be 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;

      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;

      

       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;

      

       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;

      ((A \ C) /\ D) = {} by A1, A3, XBOOLE_1: 3, XBOOLE_1: 27;

      hence (X1 /\ X4) = {} by A4, A7, XBOOLE_1: 3, XBOOLE_1: 27;

      ((B \ D) /\ C) = {} by A1, A2, XBOOLE_1: 3, XBOOLE_1: 27;

      hence (X2 /\ X3) = {} by A5, A6, XBOOLE_1: 3, XBOOLE_1: 27;

      

       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;

      thus thesis by A1, A2, A3, A6, A7, XBOOLE_1: 3, XBOOLE_1: 27;

    end;

    registration

      cluster strict Colored-PT-net-like for Colored_Petri_net;

      existence

      proof

        set PLA = { 0 };

        set a = the set;

        set TRA = {a};

        set TSA = [:TRA, PLA:];

        TSA c= TSA;

        then

        reconsider TSA as non empty Relation of TRA, PLA;

        set STA = [:PLA, TRA:];

        STA c= STA;

        then

        reconsider STA as non empty Relation of PLA, TRA;

        set CS = {a, a, a};

        set fa = the Function of ( thin_cylinders (CS, { 0 })), ( thin_cylinders (CS, { 0 }));

        set f = ( {a} --> fa);

        set CPNT = Colored_PT_net_Str (# PLA, TRA, STA, TSA, CS, f #);

        

         A1: CPNT is with_S-T_arc;

        CPNT is with_T-S_arc;

        then

        reconsider CPNT as Colored_Petri_net by A1;

        take CPNT;

         A2:

        now

          CS c= CS;

          then

          reconsider CS1 = CS as non empty Subset of the ColoredSet of CPNT;

          let t be transition of CPNT;

          assume t in ( dom the firing-rule of CPNT);

          

           A3: t = a by TARSKI:def 1;

          

           A4: a in TRA by TARSKI:def 1;

          

           A5: 0 in PLA by TARSKI:def 1;

          then [a, 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 , a] 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: fa is Function of ( thin_cylinders (CS1,I)), ( thin_cylinders (CS1,O));

          (f . t) = fa by FUNCOP_1: 7;

          hence ex CS1 be non empty Subset of the ColoredSet of CPNT, I be Subset of ( *' {t}), O be Subset of ( {t} *' ) st (the firing-rule of CPNT . t) is Function of ( thin_cylinders (CS1,I)), ( thin_cylinders (CS1,O)) by A6;

        end;

        

         A7: ( dom f) = {a} by FUNCOP_1: 13;

        now

          reconsider a1 = a as transition of CPNT by TARSKI:def 1;

          let x be object;

           0 in PLA 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);

            then ex x be transition of CPNT st a1 = x & x is outbound;

            hence contradiction by A8;

          end;

          assume x in ( dom the firing-rule of CPNT);

          then x = a by A7, TARSKI:def 1;

          hence x in (the carrier' of CPNT \ ( Outbds CPNT)) by A9, XBOOLE_0:def 5;

        end;

        then ( dom the firing-rule of CPNT) c= (the carrier' of CPNT \ ( Outbds CPNT));

        hence thesis by A2;

      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;

      :: PETRI_2:def12

      pred CPNT1 misses CPNT2 means (the carrier of CPNT1 /\ the carrier of CPNT2) = {} & (the carrier' of CPNT1 /\ the carrier' of CPNT2) = {} ;

      symmetry ;

    end

    begin

    definition

      let CPNT1 be Colored_Petri_net;

      let CPNT2 be Colored_Petri_net;

      :: PETRI_2:def13

      mode connecting-mapping of CPNT1,CPNT2 -> set means

      : Def13: ex O12 be Function of ( Outbds CPNT1), the carrier of CPNT2, O21 be Function of ( Outbds CPNT2), the carrier of CPNT1 st it = [O12, O21];

      correctness

      proof

        set O12 = the Function of ( Outbds CPNT1), the carrier of CPNT2, O21 = the Function of ( Outbds CPNT2), the carrier of CPNT1;

        set Z = [O12, O21];

        take Z;

        thus thesis;

      end;

    end

    begin

    definition

      let CPNT1,CPNT2 be Colored-PT-net;

      let O be connecting-mapping of CPNT1, CPNT2;

      :: PETRI_2:def14

      mode connecting-firing-rule of CPNT1,CPNT2,O -> set means

      : Def14: ex q12,q21 be Function, O12 be Function of ( Outbds CPNT1), the carrier of CPNT2, O21 be Function of ( Outbds CPNT2), the carrier of CPNT1 st O = [O12, O21] & ( dom q12) = ( Outbds CPNT1) & ( dom q21) = ( Outbds CPNT2) & (for t01 be 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 be 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

      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 (K1,K2));

        set Y2 = ( PFuncs (L1,L2));

        consider O12 be Function of ( Outbds CPNT1), the carrier of CPNT2, O21 be Function of ( Outbds CPNT2), the carrier of CPNT1 such that

         A1: O = [O12, O21] by Def13;

        defpred R[ object, object] means ex t02 be 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 P[ object, object] means ex t01 be 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 be object st x in TO1 holds ex y be object st y in Y1 & P[x, y]

        proof

          let x be object;

          assume x in TO1;

          then

          consider t01 be 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,t1)), ( thin_cylinders (the ColoredSet of CPNT1,t2));

          take y;

          set H1 = ( thin_cylinders (the ColoredSet of CPNT1,t1));

          set H2 = ( thin_cylinders (the ColoredSet of CPNT1,t2));

          

           A4: ( Funcs (H1,H2)) c= ( PFuncs (H1,H2)) by FUNCT_2: 72;

          

           A5: H2 c= ( bool ( PFuncs (the carrier of CPNT2,the ColoredSet of CPNT1))) by Lm1;

          H1 c= ( bool ( PFuncs (the carrier of CPNT1,the ColoredSet of CPNT1))) by Lm1;

          then

           A6: ( PFuncs (H1,H2)) c= ( PFuncs (K1,K2)) by A5, PARTFUN1: 50;

          y in ( Funcs (H1,H2)) by FUNCT_2: 8;

          then y in ( PFuncs (H1,H2)) by A4;

          hence thesis by A3, A6;

        end;

        consider q12 be Function of TO1, Y1 such that

         A7: for x be object st x in TO1 holds P[x, (q12 . x)] from FUNCT_2:sch 1( A2);

         A8:

        now

          let tt01 be transition of CPNT1;

          assume tt01 is outbound;

          then tt01 in TO1;

          then ex t01 be 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))));

        end;

        

         A9: for x be object st x in TO2 holds ex y be object st y in Y2 & R[x, y]

        proof

          let x be object;

          assume x in TO2;

          then

          consider t02 be 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,t1)), ( thin_cylinders (the ColoredSet of CPNT2,t2));

          take y;

          set H1 = ( thin_cylinders (the ColoredSet of CPNT2,t1));

          set H2 = ( thin_cylinders (the ColoredSet of CPNT2,t2));

          

           A11: ( Funcs (H1,H2)) c= ( PFuncs (H1,H2)) by FUNCT_2: 72;

          

           A12: H2 c= ( bool ( PFuncs (the carrier of CPNT1,the ColoredSet of CPNT2))) by Lm1;

          H1 c= ( bool ( PFuncs (the carrier of CPNT2,the ColoredSet of CPNT2))) by Lm1;

          then

           A13: ( PFuncs (H1,H2)) c= ( PFuncs (L1,L2)) by A12, PARTFUN1: 50;

          y in ( Funcs (H1,H2)) by FUNCT_2: 8;

          then y in ( PFuncs (H1,H2)) by A11;

          hence thesis by A10, A13;

        end;

        consider q21 be Function of TO2, Y2 such that

         A14: for x be object st x in TO2 holds R[x, (q21 . x)] from FUNCT_2:sch 1( A9);

         A15:

        now

          let tt02 be transition of CPNT2;

          assume tt02 is outbound;

          then tt02 in TO2;

          then ex t02 be 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))));

        end;

        take [q12, q21];

        

         A16: ( dom q21) = ( Outbds CPNT2) by FUNCT_2:def 1;

        ( dom q12) = ( Outbds CPNT1) by FUNCT_2:def 1;

        hence thesis by A1, A8, A15, A16;

      end;

    end

    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;

      :: PETRI_2:def15

      func synthesis (CPNT1,CPNT2,O,q) -> strict Colored-PT-net means ex q12,q21 be Function, O12 be Function of ( Outbds CPNT1), the carrier of CPNT2, O21 be Function of ( Outbds CPNT2), the carrier of CPNT1 st O = [O12, O21] & ( dom q12) = ( Outbds CPNT1) & ( dom q21) = ( Outbds CPNT2) & (for t01 be 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 be 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

      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 be Function, O12 be Function of ( Outbds CPNT1), the carrier of CPNT2, O21 be 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 be 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 be 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;

        the carrier' of CPNT1 c= T12 by XBOOLE_1: 7;

        then

         A16: ( Outbds CPNT1) c= T12;

        

         A17: (the carrier' of CPNT1 /\ the carrier' of CPNT2) = {} by A1;

        

         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, CR12 #);

        

         A25: CPNT12 is with_S-T_arc;

        CPNT12 is with_T-S_arc;

        then

        reconsider CPNT12 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;

        

         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;

        

         A31: the S-T_Arcs of CPNT2 c= the S-T_Arcs of CPNT12 by XBOOLE_1: 7;

         A32:

        now

          let x be set;

          assume x in ( dom CR12);

          then x in ( dom ((R1 +* R2) +* R3)) or x in ( dom R4) by FUNCT_4: 12;

          then x in ( dom (R1 +* R2)) or x in ( dom R3) or x in ( dom R4) by FUNCT_4: 12;

          hence x in ( dom R1) or x in ( dom R2) or x in ( dom R3) or x in ( dom R4) by FUNCT_4: 12;

        end;

        

         A33: for t be transition of CPNT12 st t in ( dom the firing-rule of CPNT12) holds ex CS be non empty Subset of the ColoredSet of CPNT12, I be Subset of ( *' {t}), O be 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;

          assume

           A34: t in ( dom the firing-rule of CPNT12);

          now

            per cases by A32, A34;

              suppose

               A35: t in ( dom the firing-rule of CPNT1);

              ( 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 be non empty Subset of the ColoredSet of CPNT1, I1 be Subset of ( *' {t1}), O1 be 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 thesis;

            end;

              suppose

               A37: t in ( dom the firing-rule of CPNT2);

              ( 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 be non empty Subset of the ColoredSet of CPNT2, I1 be Subset of ( *' {t1}), O1 be 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 thesis;

            end;

              suppose

               A39: t in ( dom q12);

              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 object;

                

                 A40: (E31 \/ E32) c= the T-S_Arcs of CPNT12 by XBOOLE_1: 7;

                assume

                 A41: x in ( Im (O12,t1));

                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;

                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 thesis by A43, A45, A44;

              end;

              then

              reconsider O = ( Im (O12,t1)) as Subset of ( {t} *' );

              ex x1 be 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 thesis;

            end;

              suppose

               A46: t in ( dom q21);

              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 object;

                

                 A47: O21 c= (E31 \/ E32) by XBOOLE_1: 7;

                assume

                 A48: x in ( Im (O21,t1));

                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;

                

                 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 thesis by A50, A52, A51;

              end;

              then

              reconsider O = ( Im (O21,t1)) as Subset of ( {t} *' );

              ex x1 be 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 thesis;

            end;

          end;

          hence thesis;

        end;

        

         A53: TS12 = (((the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21) by XBOOLE_1: 4;

         A54:

        now

          let x be object;

          ( 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 CR12);

          then x in ( dom R1) or x in ( dom R2) or x in ( dom R3) or x in ( dom R4) by A32;

          hence x in (the carrier' of CPNT1 \/ the carrier' of CPNT2) by A9, A10, A55, A56, XBOOLE_0:def 3;

        end;

        then

         A57: ( dom the firing-rule of CPNT12) c= the carrier' of CPNT12;

        ( 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 object;

          assume

           A58: x in ( dom the firing-rule of CPNT12);

          then

          reconsider t = x as transition of CPNT12 by A54;

          now

            per cases by A32, A58;

              suppose

               A59: t in ( dom RR1);

              

               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} *' ) <> {} ;

              then

               A61: ex g be object st g in ( {t1} *' ) by XBOOLE_0:def 1;

              ( {t1} *' ) c= ( {t} *' ) by A26, A27, A28, Th7;

              then not ex w be transition of CPNT12 st t = w & w is outbound by A61;

              hence not x in ( Outbds CPNT12);

            end;

              suppose

               A62: t in ( dom RR2);

              

               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} *' ) <> {} ;

              then

               A64: ex g be object st g in ( {t1} *' ) by XBOOLE_0:def 1;

              ( {t1} *' ) c= ( {t} *' ) by A29, A31, A30, Th7;

              then not (ex w be transition of CPNT12 st t = w & w is outbound) by A64;

              hence not x in ( Outbds CPNT12);

            end;

              suppose t in ( dom RR3);

              then t in ( dom O12) by A9, FUNCT_2:def 1;

              then

              consider s be object such that

               A65: [t, s] in O12 by XTUPLE_0:def 12;

              reconsider 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;

              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 not (ex w be transition of CPNT12 st t = w & w is outbound);

              hence not x in ( Outbds CPNT12);

            end;

              suppose t in ( dom RR4);

              then t in ( dom O21) by A10, FUNCT_2:def 1;

              then

              consider s be object such that

               A70: [t, s] in O21 by XTUPLE_0:def 12;

              reconsider 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;

              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 not (ex w be transition of CPNT12 st t = w & w is outbound);

              hence not x in ( Outbds CPNT12);

            end;

          end;

          hence thesis by A57, A58, XBOOLE_0:def 5;

        end;

        then CPNT12 is Colored-PT-net-like by A33;

        hence thesis by A8, A9, A10, A11, A12, A13, A53;

      end;

      uniqueness

      proof

        let CA,CB be strict Colored-PT-net;

        assume ex q12A,q21A be Function, O12A be Function of ( Outbds CPNT1), the carrier of CPNT2, O21A be Function of ( Outbds CPNT2), the carrier of CPNT1 st O = [O12A, O21A] & ( dom q12A) = ( Outbds CPNT1) & ( dom q21A) = ( Outbds CPNT2) & (for t01 be 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 be 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);

        then

        consider q12A,q21A be Function, O12A be Function of ( Outbds CPNT1), the carrier of CPNT2, O21A be 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 be 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 be 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 be Function, O12B be Function of ( Outbds CPNT1), the carrier of CPNT2, O21B be Function of ( Outbds CPNT2), the carrier of CPNT1 st O = [O12B, O21B] & ( dom q12B) = ( Outbds CPNT1) & ( dom q21B) = ( Outbds CPNT2) & (for t01 be 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 be 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);

        then

        consider q12B,q21B be Function, O12B be Function of ( Outbds CPNT1), the carrier of CPNT2, O21B be 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 be 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 be 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 thesis by A75, A77, A78, A79, A80, A81, A82, A83, A85, A86, A87, A88, A89, A90, A91, A92, XTUPLE_0: 1;

      end;

    end