circcomb.miz



    begin

    definition

      let S be ManySortedSign;

      mode Gate of S is Element of the carrier' of S;

    end

     Lm1:

    now

      let i be Element of NAT , X be non empty set;

      

      thus ( product (( Seg i) --> X)) = ( product (i |-> X)) by FINSEQ_2:def 2

      .= (i -tuples_on X) by FINSEQ_3: 131;

    end;

    registration

      let A,B be set;

      let f be ManySortedSet of A;

      let g be ManySortedSet of B;

      cluster (f +* g) -> (A \/ B) -defined;

      coherence

      proof

        

         A1: ( dom g) = B by PARTFUN1:def 2;

        ( dom f) = A by PARTFUN1:def 2;

        then ( dom (f +* g)) = (A \/ B) by A1, FUNCT_4:def 1;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let A,B be set;

      let f be ManySortedSet of A;

      let g be ManySortedSet of B;

      cluster (f +* g) -> total;

      coherence

      proof

        

         A1: ( dom g) = B by PARTFUN1:def 2;

        ( dom f) = A by PARTFUN1:def 2;

        then ( dom (f +* g)) = (A \/ B) by A1, FUNCT_4:def 1;

        hence thesis;

      end;

    end

    registration

      let A,B be set;

      cluster (A .--> B) -> {A} -defined;

      coherence ;

    end

    registration

      let A,B be set;

      cluster (A .--> B) -> total;

      coherence ;

    end

    registration

      let A be set, B be non empty set;

      cluster (A .--> B) -> non-empty;

      coherence ;

    end

    theorem :: CIRCCOMB:1

    

     Th1: for A,B be set, f be ManySortedSet of A holds for g be ManySortedSet of B st f c= g holds (f # ) c= (g # )

    proof

      let A,B be set, f be ManySortedSet of A;

      let g be ManySortedSet of B;

      assume

       A1: f c= g;

      

       A2: ( dom f) c= ( dom g) by A1, RELAT_1: 11;

      

       A3: ( dom g) = B by PARTFUN1:def 2;

      

       A4: ( dom (g # )) = (B * ) by PARTFUN1:def 2;

      let z be object;

      

       A5: ( dom f) = A by PARTFUN1:def 2;

      assume

       A6: z in (f # );

      then

      consider x,y be object such that

       A7: [x, y] = z by RELAT_1:def 1;

      ( dom (f # )) = (A * ) by PARTFUN1:def 2;

      then

      reconsider x as Element of (A * ) by A6, A7, XTUPLE_0:def 12;

      

       A8: ( rng x) c= A by FINSEQ_1:def 4;

      ( rng x) c= A by FINSEQ_1:def 4;

      then ( rng x) c= B by A5, A3, A2;

      then x is FinSequence of B by FINSEQ_1:def 4;

      then

      reconsider x9 = x as Element of (B * ) by FINSEQ_1:def 11;

      

       A9: ( rng x9) c= B by FINSEQ_1:def 4;

      y = ((f # ) . x) by A6, A7, FUNCT_1: 1

      .= ( product (f * x)) by FINSEQ_2:def 5

      .= ( product (g * x9)) by A1, A5, A3, A8, A9, PARTFUN1: 54, PARTFUN1: 79

      .= ((g # ) . x9) by FINSEQ_2:def 5;

      hence z in (g # ) by A7, A4, FUNCT_1: 1;

    end;

    theorem :: CIRCCOMB:2

    

     Th2: for X be set, Y be non empty set, p be FinSequence of X holds (((X --> Y) # ) . p) = (( len p) -tuples_on Y)

    proof

      let X be set, Y be non empty set, p be FinSequence of X;

      ( rng p) c= X by FINSEQ_1:def 4;

      then (( rng p) /\ X) = ( rng p) by XBOOLE_1: 28;

      

      then

       A1: (p " X) = (p " ( rng p)) by RELAT_1: 133

      .= ( dom p) by RELAT_1: 134;

      p in (X * ) by FINSEQ_1:def 11;

      

      hence (((X --> Y) # ) . p) = ( product ((X --> Y) * p)) by FINSEQ_2:def 5

      .= ( product ((p " X) --> Y)) by FUNCOP_1: 19

      .= ( product (( Seg ( len p)) --> Y)) by A1, FINSEQ_1:def 3

      .= (( len p) -tuples_on Y) by Lm1;

    end;

    definition

      let A be set;

      let f1,g1 be non-empty ManySortedSet of A;

      let B be set;

      let f2,g2 be non-empty ManySortedSet of B;

      let h1 be ManySortedFunction of f1, g1;

      let h2 be ManySortedFunction of f2, g2;

      :: original: +*

      redefine

      func h1 +* h2 -> ManySortedFunction of (f1 +* f2), (g1 +* g2) ;

      coherence

      proof

        set f = (f1 +* f2), g = (g1 +* g2), h = (h1 +* h2);

        

         A1: ( dom g1) = A by PARTFUN1:def 2;

        

         A2: ( dom f2) = B by PARTFUN1:def 2;

        

         A3: ( dom g2) = B by PARTFUN1:def 2;

        

         A4: ( dom h2) = B by PARTFUN1:def 2;

        

         A5: ( dom h1) = A by PARTFUN1:def 2;

        reconsider h as ManySortedFunction of (A \/ B);

        

         A6: ( dom f1) = A by PARTFUN1:def 2;

        h is ManySortedFunction of f, g

        proof

          let x be object;

          

           A7: not x in B or x in B;

          assume

           A8: x in (A \/ B);

          then x in A or x in B by XBOOLE_0:def 3;

          then (h . x) = (h1 . x) & (h1 . x) is Function of (f1 . x), (g1 . x) & (f . x) = (f1 . x) & (g . x) = (g1 . x) or (h . x) = (h2 . x) & (h2 . x) is Function of (f2 . x), (g2 . x) & (f . x) = (f2 . x) & (g . x) = (g2 . x) by A6, A1, A5, A2, A3, A4, A8, A7, FUNCT_4:def 1, PBOOLE:def 15;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let S1,S2 be ManySortedSign;

      :: CIRCCOMB:def1

      pred S1 tolerates S2 means the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2;

      reflexivity ;

      symmetry ;

    end

    definition

      let S1,S2 be non empty ManySortedSign;

      :: CIRCCOMB:def2

      func S1 +* S2 -> strict non empty ManySortedSign means

      : Def2: the carrier of it = (the carrier of S1 \/ the carrier of S2) & the carrier' of it = (the carrier' of S1 \/ the carrier' of S2) & the Arity of it = (the Arity of S1 +* the Arity of S2) & the ResultSort of it = (the ResultSort of S1 +* the ResultSort of S2);

      existence

      proof

        set RESULT = (the ResultSort of S1 +* the ResultSort of S2);

        set ARITY = (the Arity of S1 +* the Arity of S2);

        set OPER = (the carrier' of S1 \/ the carrier' of S2);

        reconsider CARR = (the carrier of S1 \/ the carrier of S2) as non empty set;

        

         A1: ( dom the ResultSort of S2) = the carrier' of S2 by FUNCT_2:def 1;

        ( dom the ResultSort of S1) = the carrier' of S1 by FUNCT_2:def 1;

        then

         A2: ( dom RESULT) = OPER by A1, FUNCT_4:def 1;

        

         A3: the carrier of S1 c= CARR by XBOOLE_1: 7;

        

         A4: the carrier of S2 c= CARR by XBOOLE_1: 7;

        ( rng the ResultSort of S2) c= the carrier of S2 by RELAT_1:def 19;

        then

         A5: ( rng the ResultSort of S2) c= CARR by A4;

        ( rng the ResultSort of S1) c= the carrier of S1 by RELAT_1:def 19;

        then ( rng the ResultSort of S1) c= CARR by A3;

        then

         A6: (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2)) c= CARR by A5, XBOOLE_1: 8;

        ( rng RESULT) c= (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2)) by FUNCT_4: 17;

        then ( rng RESULT) c= CARR by A6;

        then

        reconsider RESULT as Function of OPER, CARR by A2, FUNCT_2:def 1, RELSET_1: 4;

        

         A7: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

        ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

        then

         A8: ( dom ARITY) = OPER by A7, FUNCT_4:def 1;

        

         A9: ( rng the Arity of S1) c= (the carrier of S1 * ) by RELAT_1:def 19;

        

         A10: ( rng the Arity of S2) c= (the carrier of S2 * ) by RELAT_1:def 19;

        (the carrier of S2 * ) c= (CARR * ) by FINSEQ_1: 62, XBOOLE_1: 7;

        then

         A11: ( rng the Arity of S2) c= (CARR * ) by A10;

        (the carrier of S1 * ) c= (CARR * ) by FINSEQ_1: 62, XBOOLE_1: 7;

        then ( rng the Arity of S1) c= (CARR * ) by A9;

        then

         A12: (( rng the Arity of S1) \/ ( rng the Arity of S2)) c= (CARR * ) by A11, XBOOLE_1: 8;

        ( rng ARITY) c= (( rng the Arity of S1) \/ ( rng the Arity of S2)) by FUNCT_4: 17;

        then ( rng ARITY) c= (CARR * ) by A12;

        then

        reconsider ARITY as Function of OPER, (CARR * ) by A8, FUNCT_2:def 1, RELSET_1: 4;

        take ManySortedSign (# CARR, OPER, ARITY, RESULT #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: CIRCCOMB:3

    

     Th3: for S1,S2,S3 be non empty ManySortedSign st S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 holds (S1 +* S2) tolerates S3

    proof

      let S1,S2,S3 be non empty ManySortedSign such that

       A1: the Arity of S1 tolerates the Arity of S2 and

       A2: the ResultSort of S1 tolerates the ResultSort of S2 and

       A3: the Arity of S2 tolerates the Arity of S3 and

       A4: the ResultSort of S2 tolerates the ResultSort of S3 and

       A5: the Arity of S3 tolerates the Arity of S1 and

       A6: the ResultSort of S3 tolerates the ResultSort of S1;

      the Arity of (S1 +* S2) = (the Arity of S1 +* the Arity of S2) by Def2;

      hence the Arity of (S1 +* S2) tolerates the Arity of S3 by A1, A3, A5, FUNCT_4: 125;

      the ResultSort of (S1 +* S2) = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

      hence thesis by A2, A4, A6, FUNCT_4: 125;

    end;

    theorem :: CIRCCOMB:4

    for S be non empty ManySortedSign holds (S +* S) = the ManySortedSign of S

    proof

      let S be non empty ManySortedSign;

      

       A1: the carrier' of S = (the carrier' of S \/ the carrier' of S);

      

       A2: the Arity of S = (the Arity of S +* the Arity of S);

      

       A3: the ResultSort of S = (the ResultSort of S +* the ResultSort of S);

      the carrier of S = (the carrier of S \/ the carrier of S);

      hence thesis by A1, A2, A3, Def2;

    end;

    theorem :: CIRCCOMB:5

    

     Th5: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 holds (S1 +* S2) = (S2 +* S1)

    proof

      let S1,S2 be non empty ManySortedSign;

      set S = (S1 +* S2);

      assume that

       A1: the Arity of S1 tolerates the Arity of S2 and

       A2: the ResultSort of S1 tolerates the ResultSort of S2;

      

       A3: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      (the ResultSort of S1 +* the ResultSort of S2) = (the ResultSort of S2 +* the ResultSort of S1) by A2, FUNCT_4: 34;

      then

       A4: the ResultSort of S = (the ResultSort of S2 +* the ResultSort of S1) by Def2;

      (the Arity of S1 +* the Arity of S2) = (the Arity of S2 +* the Arity of S1) by A1, FUNCT_4: 34;

      then

       A5: the Arity of S = (the Arity of S2 +* the Arity of S1) by Def2;

      the carrier of S = (the carrier of S1 \/ the carrier of S2) by Def2;

      hence thesis by A3, A5, A4, Def2;

    end;

    theorem :: CIRCCOMB:6

    for S1,S2,S3 be non empty ManySortedSign holds ((S1 +* S2) +* S3) = (S1 +* (S2 +* S3))

    proof

      let S1,S2,S3 be non empty ManySortedSign;

      set S12 = (S1 +* S2), S23 = (S2 +* S3);

      set S1293 = (S12 +* S3), S1923 = (S1 +* S23);

      

       A1: the carrier of S23 = (the carrier of S2 \/ the carrier of S3) by Def2;

      

       A2: the carrier of S1293 = (the carrier of S12 \/ the carrier of S3) by Def2;

      

       A3: the carrier of S1923 = (the carrier of S1 \/ the carrier of S23) by Def2;

      the carrier of S12 = (the carrier of S1 \/ the carrier of S2) by Def2;

      then

       A4: the carrier of S1293 = the carrier of S1923 by A1, A2, A3, XBOOLE_1: 4;

      

       A5: the carrier' of S23 = (the carrier' of S2 \/ the carrier' of S3) by Def2;

      

       A6: the carrier' of S1293 = (the carrier' of S12 \/ the carrier' of S3) by Def2;

      

       A7: the Arity of S23 = (the Arity of S2 +* the Arity of S3) by Def2;

      

       A8: the Arity of S1923 = (the Arity of S1 +* the Arity of S23) by Def2;

      

       A9: the carrier' of S1923 = (the carrier' of S1 \/ the carrier' of S23) by Def2;

      the carrier' of S12 = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      then

       A10: the carrier' of S1293 = the carrier' of S1923 by A5, A6, A9, XBOOLE_1: 4;

      

       A11: the ResultSort of S1923 = (the ResultSort of S1 +* the ResultSort of S23) by Def2;

      

       A12: the ResultSort of S1293 = (the ResultSort of S12 +* the ResultSort of S3) by Def2;

      

       A13: the Arity of S1293 = (the Arity of S12 +* the Arity of S3) by Def2;

      the Arity of S12 = (the Arity of S1 +* the Arity of S2) by Def2;

      then

       A14: the Arity of S1293 = the Arity of S1923 by A7, A13, A8, FUNCT_4: 14;

      

       A15: the ResultSort of S23 = (the ResultSort of S2 +* the ResultSort of S3) by Def2;

      the ResultSort of S12 = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

      hence thesis by A15, A12, A11, A4, A10, A14, FUNCT_4: 14;

    end;

    theorem :: CIRCCOMB:7

    for f be one-to-one Function holds for S1,S2 be Circuit-like non empty ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds (S1 +* S2) is Circuit-like

    proof

      let f be one-to-one Function;

      let S1,S2 be Circuit-like non empty ManySortedSign such that

       A1: the ResultSort of S1 c= f and

       A2: the ResultSort of S2 c= f;

      let S be non void non empty ManySortedSign;

      set r1 = the ResultSort of S1, r2 = the ResultSort of S2;

      set r = the ResultSort of S;

      

       A3: (r1 +* r2) c= (r1 \/ r2) by FUNCT_4: 29;

      assume S = (S1 +* S2);

      then

       A4: r = (r1 +* r2) by Def2;

      (r1 \/ r2) c= f by A1, A2, XBOOLE_1: 8;

      then

       A5: (r1 +* r2) c= f by A3;

      then

       A6: ( dom r) c= ( dom f) by A4, GRFUNC_1: 2;

      let o1,o2 be Gate of S;

      

       A7: ( dom r) = the carrier' of S by FUNCT_2:def 1;

      then

       A8: o1 in ( dom r);

      

       A9: o2 in ( dom r) by A7;

      assume

       A10: ( the_result_sort_of o1) = ( the_result_sort_of o2);

      

       A11: (r . o2) = (f . o2) by A4, A7, A5, GRFUNC_1: 2;

      (r . o1) = (f . o1) by A4, A7, A5, GRFUNC_1: 2;

      hence thesis by A10, A8, A9, A11, A6, FUNCT_1:def 4;

    end;

    theorem :: CIRCCOMB:8

    for S1,S2 be Circuit-like non empty ManySortedSign st ( InnerVertices S1) misses ( InnerVertices S2) holds (S1 +* S2) is Circuit-like

    proof

      let S1,S2 be Circuit-like non empty ManySortedSign;

      assume

       A1: ( InnerVertices S1) misses ( InnerVertices S2);

      set r1 = the ResultSort of S1, r2 = the ResultSort of S2;

      let S be non void non empty ManySortedSign;

      set r = the ResultSort of S;

      

       A2: ( dom r1) = the carrier' of S1 by FUNCT_2:def 1;

      assume

       A3: S = (S1 +* S2);

      then

       A4: r = (r1 +* r2) by Def2;

      

       A5: ( dom r2) = the carrier' of S2 by FUNCT_2:def 1;

      let o1,o2 be Gate of S;

      

       A6: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by A3, Def2;

      then not o1 in the carrier' of S2 & o1 in the carrier' of S1 or o1 in the carrier' of S2 by XBOOLE_0:def 3;

      then

       A7: (r . o1) = (r1 . o1) & (r1 . o1) in ( rng r1) & o1 in the carrier' of S1 or (r . o1) = (r2 . o1) & (r2 . o1) in ( rng r2) & o1 in the carrier' of S2 by A4, A2, A5, A6, FUNCT_1:def 3, FUNCT_4:def 1;

       not o2 in the carrier' of S2 & o2 in the carrier' of S1 or o2 in the carrier' of S2 by A6, XBOOLE_0:def 3;

      then

       A8: (r . o2) = (r1 . o2) & (r1 . o2) in ( rng r1) & o2 in the carrier' of S1 or (r . o2) = (r2 . o2) & (r2 . o2) in ( rng r2) & o2 in the carrier' of S2 by A4, A2, A5, A6, FUNCT_1:def 3, FUNCT_4:def 1;

      assume

       A9: ( the_result_sort_of o1) = ( the_result_sort_of o2);

      per cases by A1, A9, A7, A8, XBOOLE_0: 3;

        suppose

         A10: (r . o1) = (r1 . o1) & o1 in the carrier' of S1 & (r . o2) = (r1 . o2) & o2 in the carrier' of S1;

        then

        reconsider S = S1 as non void Circuit-like non empty ManySortedSign;

        reconsider p1 = o1, p2 = o2 as Gate of S by A10;

        

         A11: ( the_result_sort_of p2) = (r1 . p2);

        ( the_result_sort_of p1) = (r1 . p1);

        hence thesis by A9, A10, A11, MSAFREE2:def 6;

      end;

        suppose

         A12: (r . o1) = (r2 . o1) & o1 in the carrier' of S2 & (r . o2) = (r2 . o2) & o2 in the carrier' of S2;

        then

        reconsider S = S2 as non void Circuit-like non empty ManySortedSign;

        reconsider p1 = o1, p2 = o2 as Gate of S by A12;

        

         A13: ( the_result_sort_of p2) = (r2 . p2);

        ( the_result_sort_of p1) = (r2 . p1);

        hence thesis by A9, A12, A13, MSAFREE2:def 6;

      end;

    end;

    theorem :: CIRCCOMB:9

    

     Th9: for S1,S2 be non empty ManySortedSign st not S1 is void or not S2 is void holds (S1 +* S2) is non void

    proof

      let S1,S2 be non empty ManySortedSign;

      assume

       A1: not S1 is void or not S2 is void;

      the carrier' of (S1 +* S2) = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      hence the carrier' of (S1 +* S2) is non empty by A1;

    end;

    theorem :: CIRCCOMB:10

    for S1,S2 be finite non empty ManySortedSign holds (S1 +* S2) is finite

    proof

      let S1,S2 be finite non empty ManySortedSign;

      reconsider C1 = the carrier of S1, C2 = the carrier of S2 as finite set;

      the carrier of (S1 +* S2) = (C1 \/ C2) by Def2;

      hence thesis;

    end;

    registration

      let S1 be non void non empty ManySortedSign;

      let S2 be non empty ManySortedSign;

      cluster (S1 +* S2) -> non void;

      coherence by Th9;

      cluster (S2 +* S1) -> non void;

      coherence by Th9;

    end

    theorem :: CIRCCOMB:11

    

     Th11: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 holds ( InnerVertices (S1 +* S2)) = (( InnerVertices S1) \/ ( InnerVertices S2)) & ( InputVertices (S1 +* S2)) c= (( InputVertices S1) \/ ( InputVertices S2))

    proof

      let S1,S2 be non empty ManySortedSign;

      set R1 = the ResultSort of S1, R2 = the ResultSort of S2;

      assume that the Arity of S1 tolerates the Arity of S2 and

       A1: R1 tolerates R2;

      set S = (S1 +* S2), R = the ResultSort of S;

      

       A2: R = (R1 +* R2) by Def2;

      then R1 c= R by A1, FUNCT_4: 28;

      then

       A3: ( rng R1) c= ( rng R) by RELAT_1: 11;

      ( rng R2) c= ( rng R) by A2, FUNCT_4: 18;

      then

       A4: (( rng R1) \/ ( rng R2)) c= ( rng R) by A3, XBOOLE_1: 8;

      

       A5: ( rng R) c= (( rng R1) \/ ( rng R2)) by A2, FUNCT_4: 17;

      hence ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by A4;

      let x be object;

      assume

       A6: x in ( InputVertices S);

      then

       A7: not x in ( rng R) by XBOOLE_0:def 5;

      

       A8: ( rng R) = (( rng R1) \/ ( rng R2)) by A5, A4;

      then

       A9: not x in ( rng R2) by A7, XBOOLE_0:def 3;

      the carrier of S = (the carrier of S1 \/ the carrier of S2) by Def2;

      then

       A10: x in the carrier of S1 or x in the carrier of S2 by A6, XBOOLE_0:def 3;

       not x in ( rng R1) by A8, A7, XBOOLE_0:def 3;

      then x in (the carrier of S1 \ ( rng R1)) or x in (the carrier of S2 \ ( rng R2)) by A10, A9, XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CIRCCOMB:12

    

     Th12: for S1,S2 be non empty ManySortedSign holds for v2 be Vertex of S2 st v2 in ( InputVertices (S1 +* S2)) holds v2 in ( InputVertices S2)

    proof

      let S1,S2 be non empty ManySortedSign;

      set R1 = the ResultSort of S1, R2 = the ResultSort of S2;

      set S = (S1 +* S2), R = the ResultSort of S;

      let v2 be Vertex of S2;

      R = (R1 +* R2) by Def2;

      then

       A1: ( rng R2) c= ( rng R) by FUNCT_4: 18;

      assume v2 in ( InputVertices S);

      then not v2 in ( rng R2) by A1, XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: CIRCCOMB:13

    

     Th13: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 holds for v1 be Vertex of S1 st v1 in ( InputVertices (S1 +* S2)) holds v1 in ( InputVertices S1)

    proof

      let S1,S2 be non empty ManySortedSign such that the Arity of S1 tolerates the Arity of S2 and

       A1: the ResultSort of S1 tolerates the ResultSort of S2;

      set S = (S1 +* S2), R = the ResultSort of S;

      set R1 = the ResultSort of S1, R2 = the ResultSort of S2;

      R = (R1 +* R2) by Def2;

      then R1 c= R by A1, FUNCT_4: 28;

      then

       A2: ( rng R1) c= ( rng R) by RELAT_1: 11;

      let v1 be Vertex of S1;

      assume v1 in ( InputVertices S);

      then not v1 in ( rng R1) by A2, XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: CIRCCOMB:14

    

     Th14: for S1 be non empty ManySortedSign, S2 be non void non empty ManySortedSign holds for o2 be OperSymbol of S2, o be OperSymbol of (S1 +* S2) st o2 = o holds ( the_arity_of o) = ( the_arity_of o2) & ( the_result_sort_of o) = ( the_result_sort_of o2)

    proof

      let S1 be non empty ManySortedSign;

      let S2 be non void non empty ManySortedSign;

      let o2 be OperSymbol of S2, o be OperSymbol of (S1 +* S2);

      assume

       A1: o2 = o;

      

       A2: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

      the Arity of (S1 +* S2) = (the Arity of S1 +* the Arity of S2) by Def2;

      hence ( the_arity_of o) = ( the_arity_of o2) by A1, A2, FUNCT_4: 13;

      

       A3: ( dom the ResultSort of S2) = the carrier' of S2 by FUNCT_2:def 1;

      the ResultSort of (S1 +* S2) = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

      hence thesis by A1, A3, FUNCT_4: 13;

    end;

    theorem :: CIRCCOMB:15

    

     Th15: for S1 be non empty ManySortedSign, S2,S be Circuit-like non void non empty ManySortedSign st S = (S1 +* S2) holds for v2 be Vertex of S2 st v2 in ( InnerVertices S2) holds for v be Vertex of S st v2 = v holds v in ( InnerVertices S) & ( action_at v) = ( action_at v2)

    proof

      let S1 be non empty ManySortedSign, S2,S be Circuit-like non void non empty ManySortedSign such that

       A1: S = (S1 +* S2);

      let v2 be Vertex of S2 such that

       A2: v2 in ( InnerVertices S2);

      the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by A1, Def2;

      then

      reconsider o = ( action_at v2) as OperSymbol of S by XBOOLE_0:def 3;

      let v be Vertex of S such that

       A3: v2 = v;

      the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by A1, Def2;

      then

       A4: ( InnerVertices S2) c= ( InnerVertices S) by FUNCT_4: 18;

      hence v in ( InnerVertices S) by A2, A3;

      ( the_result_sort_of ( action_at v2)) = v2 by A2, MSAFREE2:def 7;

      then v = ( the_result_sort_of o) by A1, A3, Th14;

      hence thesis by A2, A3, A4, MSAFREE2:def 7;

    end;

    theorem :: CIRCCOMB:16

    

     Th16: for S1 be non void non empty ManySortedSign, S2 be non empty ManySortedSign st S1 tolerates S2 holds for o1 be OperSymbol of S1, o be OperSymbol of (S1 +* S2) st o1 = o holds ( the_arity_of o) = ( the_arity_of o1) & ( the_result_sort_of o) = ( the_result_sort_of o1)

    proof

      let S1 be non void non empty ManySortedSign, S2 be non empty ManySortedSign such that

       A1: the Arity of S1 tolerates the Arity of S2 and

       A2: the ResultSort of S1 tolerates the ResultSort of S2;

      let o1 be OperSymbol of S1, o be OperSymbol of (S1 +* S2);

      assume

       A3: o1 = o;

      

       A4: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

      the Arity of (S1 +* S2) = (the Arity of S1 +* the Arity of S2) by Def2;

      hence ( the_arity_of o) = ( the_arity_of o1) by A1, A3, A4, FUNCT_4: 15;

      

       A5: ( dom the ResultSort of S1) = the carrier' of S1 by FUNCT_2:def 1;

      the ResultSort of (S1 +* S2) = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

      hence thesis by A2, A3, A5, FUNCT_4: 15;

    end;

    theorem :: CIRCCOMB:17

    

     Th17: for S1,S be Circuit-like non void non empty ManySortedSign, S2 be non empty ManySortedSign st S1 tolerates S2 & S = (S1 +* S2) holds for v1 be Vertex of S1 st v1 in ( InnerVertices S1) holds for v be Vertex of S st v1 = v holds v in ( InnerVertices S) & ( action_at v) = ( action_at v1)

    proof

      let S1,S be Circuit-like non void non empty ManySortedSign, S2 be non empty ManySortedSign such that

       A1: S1 tolerates S2 and

       A2: S = (S1 +* S2);

      let v1 be Vertex of S1 such that

       A3: v1 in ( InnerVertices S1);

      let v be Vertex of S such that

       A4: v1 = v;

      ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by A1, A2, Th11;

      hence

       A5: v in ( InnerVertices S) by A3, A4, XBOOLE_0:def 3;

      the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by A2, Def2;

      then

      reconsider o = ( action_at v1) as OperSymbol of S by XBOOLE_0:def 3;

      ( the_result_sort_of ( action_at v1)) = v1 by A3, MSAFREE2:def 7;

      then v = ( the_result_sort_of o) by A1, A2, A4, Th16;

      hence thesis by A5, MSAFREE2:def 7;

    end;

    begin

    definition

      let S1,S2 be non empty ManySortedSign;

      let A1 be MSAlgebra over S1;

      let A2 be MSAlgebra over S2;

      :: CIRCCOMB:def3

      pred A1 tolerates A2 means S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2;

    end

    definition

      let S1,S2 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1;

      let A2 be non-empty MSAlgebra over S2;

      assume

       A1: the Sorts of A1 tolerates the Sorts of A2;

      :: CIRCCOMB:def4

      func A1 +* A2 -> strict non-empty MSAlgebra over (S1 +* S2) means

      : Def4: the Sorts of it = (the Sorts of A1 +* the Sorts of A2) & the Charact of it = (the Charact of A1 +* the Charact of A2);

      uniqueness ;

      existence

      proof

        set CHARACT = (the Charact of A1 +* the Charact of A2);

        set SA1 = the Sorts of A1, SA2 = the Sorts of A2;

        set S = (S1 +* S2);

        set I = the carrier of S, I1 = the carrier of S1, I2 = the carrier of S2;

        set SA12 = ((SA1 # ) +* (SA2 # ));

        

         A2: ( dom (SA2 # )) = (I2 * ) by PARTFUN1:def 2;

        

         A3: the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

        

         A4: ( rng the ResultSort of S2) c= I2 by RELAT_1:def 19;

        

         A5: ( dom SA2) = I2 by PARTFUN1:def 2;

        the carrier of S = (the carrier of S1 \/ the carrier of S2) by Def2;

        then

        reconsider SORTS = (the Sorts of A1 +* the Sorts of A2) as non-empty ManySortedSet of the carrier of (S1 +* S2);

        

         A6: ( dom (SORTS # )) = (I * ) by PARTFUN1:def 2;

        

         A7: SORTS = (SA1 \/ SA2) by A1, FUNCT_4: 30;

        then

         A8: (SA2 # ) c= (SORTS # ) by Th1, XBOOLE_1: 7;

        

         A9: ( dom SA12) = ((I1 * ) \/ (I2 * )) by PARTFUN1:def 2;

        

         A10: ( dom SA1) = I1 by PARTFUN1:def 2;

        ( rng the ResultSort of S1) c= I1 by RELAT_1:def 19;

        then

         A11: ((SA1 +* SA2) * (the ResultSort of S1 +* the ResultSort of S2)) = ((SA1 * the ResultSort of S1) +* (SA2 * the ResultSort of S2)) by A1, A10, A5, A4, FUNCT_4: 69;

        

         A12: ( rng the Arity of S2) c= (I2 * ) by RELAT_1:def 19;

        

         A13: ( dom (SA1 # )) = (I1 * ) by PARTFUN1:def 2;

        

         A14: (SA1 # ) tolerates (SA2 # )

        proof

          let x be object;

          assume

           A15: x in (( dom (SA1 # )) /\ ( dom (SA2 # )));

          then

          reconsider i1 = x as Element of (I1 * ) by A13, XBOOLE_0:def 4;

          reconsider i2 = x as Element of (I2 * ) by A2, A15, XBOOLE_0:def 4;

          

           A16: ( rng i1) c= I1 by FINSEQ_1:def 4;

          

           A17: ( rng i2) c= I2 by FINSEQ_1:def 4;

          

          thus ((SA1 # ) . x) = ( product (SA1 * i1)) by FINSEQ_2:def 5

          .= ( product (SA2 * i2)) by A1, A10, A5, A16, A17, PARTFUN1: 79

          .= ((SA2 # ) . x) by FINSEQ_2:def 5;

        end;

        then

         A18: SA12 = ((SA1 # ) \/ (SA2 # )) by FUNCT_4: 30;

        (SA1 # ) c= (SORTS # ) by A7, Th1, XBOOLE_1: 7;

        then

         A19: SA12 c= (SORTS # ) by A18, A8, XBOOLE_1: 8;

        

         A20: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

        

         A21: ( rng the Arity of S) c= (I * ) by RELAT_1:def 19;

        

         A22: ( rng the Arity of S1) c= (I1 * ) by RELAT_1:def 19;

        then

         A23: (( rng the Arity of S1) \/ ( rng the Arity of S2)) c= ((I1 * ) \/ (I2 * )) by A12, XBOOLE_1: 13;

        

         A24: the Arity of S = (the Arity of S1 +* the Arity of S2) by Def2;

        then ( rng the Arity of S) c= (( rng the Arity of S1) \/ ( rng the Arity of S2)) by FUNCT_4: 17;

        then

         A25: ( rng the Arity of S) c= ( dom SA12) by A23, A9;

        

         A26: SA12 tolerates (SORTS # ) by A19, PARTFUN1: 54;

        

         A27: (((SA1 # ) +* (SA2 # )) * (the Arity of S1 +* the Arity of S2)) = (((SA1 # ) * the Arity of S1) +* ((SA2 # ) * the Arity of S2)) by A13, A2, A22, A12, A14, FUNCT_4: 69;

        reconsider CHARACT as ManySortedFunction of ((SORTS # ) * the Arity of S), (SORTS * the ResultSort of S) by A20, A24, A3, A6, A21, A25, A11, A26, A27, PARTFUN1: 79;

        reconsider A = MSAlgebra (# SORTS, CHARACT #) as strict non-empty MSAlgebra over S by MSUALG_1:def 3;

        take A;

        thus thesis;

      end;

    end

    theorem :: CIRCCOMB:18

    for S be non void non empty ManySortedSign, A be MSAlgebra over S holds A tolerates A;

    theorem :: CIRCCOMB:19

    

     Th19: for S1,S2 be non void non empty ManySortedSign holds for A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 tolerates A2 holds A2 tolerates A1;

    theorem :: CIRCCOMB:20

    for S1,S2,S3 be non empty ManySortedSign, A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3 be MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds (A1 +* A2) tolerates A3

    proof

      let S1,S2,S3 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3 be MSAlgebra over S3 such that

       A1: S1 tolerates S2 and

       A2: the Sorts of A1 tolerates the Sorts of A2 and

       A3: the Charact of A1 tolerates the Charact of A2 and

       A4: S2 tolerates S3 and

       A5: the Sorts of A2 tolerates the Sorts of A3 and

       A6: the Charact of A2 tolerates the Charact of A3 and

       A7: S3 tolerates S1 and

       A8: the Sorts of A3 tolerates the Sorts of A1 and

       A9: the Charact of A3 tolerates the Charact of A1;

      thus (S1 +* S2) tolerates S3 by A1, A4, A7, Th3;

      the Sorts of (A1 +* A2) = (the Sorts of A1 +* the Sorts of A2) by A2, Def4;

      hence the Sorts of (A1 +* A2) tolerates the Sorts of A3 by A2, A5, A8, FUNCT_4: 125;

      the Charact of (A1 +* A2) = (the Charact of A1 +* the Charact of A2) by A2, Def4;

      hence thesis by A3, A6, A9, FUNCT_4: 125;

    end;

    theorem :: CIRCCOMB:21

    for S be strict non empty ManySortedSign, A be non-empty MSAlgebra over S holds (A +* A) = the MSAlgebra of A

    proof

      let S be strict non empty ManySortedSign, A be non-empty MSAlgebra over S;

      set A9 = the MSAlgebra of A;

      set SA = the Sorts of A9, CA = the Charact of A9;

      set SAA = the Sorts of (A +* A), CAA = the Charact of (A +* A);

      CA = (CA +* CA);

      then

       A1: CAA = CA by Def4;

      SA = (SA +* SA);

      then SAA = SA by Def4;

      hence thesis by A1;

    end;

    theorem :: CIRCCOMB:22

    

     Th22: for S1,S2 be non empty ManySortedSign, A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st A1 tolerates A2 holds (A1 +* A2) = (A2 +* A1)

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;

      set A = (A1 +* A2);

      assume that

       A1: S1 tolerates S2 and

       A2: the Sorts of A1 tolerates the Sorts of A2 and

       A3: the Charact of A1 tolerates the Charact of A2;

      (the Sorts of A1 +* the Sorts of A2) = (the Sorts of A2 +* the Sorts of A1) by A2, FUNCT_4: 34;

      then

       A4: the Sorts of A = (the Sorts of A2 +* the Sorts of A1) by A2, Def4;

      (the Charact of A1 +* the Charact of A2) = (the Charact of A2 +* the Charact of A1) by A3, FUNCT_4: 34;

      then

       A5: the Charact of A = (the Charact of A2 +* the Charact of A1) by A2, Def4;

      (S1 +* S2) = (S2 +* S1) by A1, Th5;

      hence thesis by A2, A4, A5, Def4;

    end;

    theorem :: CIRCCOMB:23

    for S1,S2,S3 be non empty ManySortedSign, A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3 be non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds ((A1 +* A2) +* A3) = (A1 +* (A2 +* A3))

    proof

      let S1,S2,S3 be non empty ManySortedSign, A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3 be non-empty MSAlgebra over S3 such that

       A1: the Sorts of A1 tolerates the Sorts of A2 and

       A2: the Sorts of A2 tolerates the Sorts of A3 and

       A3: the Sorts of A3 tolerates the Sorts of A1;

      set A12 = (A1 +* A2), A23 = (A2 +* A3);

      

       A4: the Charact of A12 = (the Charact of A1 +* the Charact of A2) by A1, Def4;

      set A1293 = (A12 +* A3), A1923 = (A1 +* A23);

      set s1 = the Sorts of A1, s2 = the Sorts of A2, s3 = the Sorts of A3;

      

       A5: the Sorts of A23 = (the Sorts of A2 +* the Sorts of A3) by A2, Def4;

      

       A6: the Sorts of A1 tolerates the Sorts of A23

      proof

        let x be object;

        assume

         A7: x in (( dom s1) /\ ( dom the Sorts of A23));

        then x in ( dom the Sorts of A23) by XBOOLE_0:def 4;

        then

         A8: x in ( dom s2) or x in ( dom s3) by A5, FUNCT_4: 12;

        x in ( dom s1) by A7, XBOOLE_0:def 4;

        then x in (( dom s1) /\ ( dom s2)) & ((s2 +* s3) . x) = (s2 . x) or x in (( dom s3) /\ ( dom s1)) & ((s2 +* s3) . x) = (s3 . x) by A2, A8, FUNCT_4: 13, FUNCT_4: 15, XBOOLE_0:def 4;

        hence thesis by A1, A3, A5;

      end;

      then

       A9: the Sorts of A1923 = (the Sorts of A1 +* the Sorts of A23) by Def4;

      

       A10: the Charact of A23 = (the Charact of A2 +* the Charact of A3) by A2, Def4;

      

       A11: the Charact of A1923 = (the Charact of A1 +* the Charact of A23) by A6, Def4;

      

       A12: the Sorts of A12 = (the Sorts of A1 +* the Sorts of A2) by A1, Def4;

      

       A13: the Sorts of A12 tolerates the Sorts of A3

      proof

        let x be object;

        assume

         A14: x in (( dom the Sorts of A12) /\ ( dom s3));

        then x in ( dom the Sorts of A12) by XBOOLE_0:def 4;

        then

         A15: x in ( dom s1) or x in ( dom s2) by A12, FUNCT_4: 12;

        x in ( dom s3) by A14, XBOOLE_0:def 4;

        then x in (( dom s3) /\ ( dom s1)) & ((s1 +* s2) . x) = (s1 . x) or x in (( dom s2) /\ ( dom s3)) & ((s1 +* s2) . x) = (s2 . x) by A1, A15, FUNCT_4: 13, FUNCT_4: 15, XBOOLE_0:def 4;

        hence thesis by A2, A3, A12;

      end;

      then the Charact of A1293 = (the Charact of A12 +* the Charact of A3) by Def4;

      then

       A16: the Charact of A1293 = the Charact of A1923 by A4, A10, A11, FUNCT_4: 14;

      the Sorts of A1293 = (the Sorts of A12 +* the Sorts of A3) by A13, Def4;

      then the Sorts of A1293 = the Sorts of A1923 by A12, A5, A9, FUNCT_4: 14;

      hence thesis by A16;

    end;

    theorem :: CIRCCOMB:24

    for S1,S2 be non empty ManySortedSign holds for A1 be finite-yielding non-empty MSAlgebra over S1 holds for A2 be finite-yielding non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds (A1 +* A2) is finite-yielding

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be finite-yielding non-empty MSAlgebra over S1, A2 be finite-yielding non-empty MSAlgebra over S2 such that

       A1: the Sorts of A1 tolerates the Sorts of A2;

      let x be object;

      set A = (A1 +* A2);

      set SA = the Sorts of A, SA1 = the Sorts of A1, SA2 = the Sorts of A2;

      

       A2: ( dom SA1) = the carrier of S1 by PARTFUN1:def 2;

      

       A3: SA1 is finite-yielding by MSAFREE2:def 11;

      assume x in the carrier of (S1 +* S2);

      then

      reconsider x as Vertex of (S1 +* S2);

      

       A4: ( dom SA2) = the carrier of S2 by PARTFUN1:def 2;

      the carrier of (S1 +* S2) = (the carrier of S1 \/ the carrier of S2) by Def2;

      then

       A5: x in the carrier of S1 or x in the carrier of S2 by XBOOLE_0:def 3;

      

       A6: SA2 is finite-yielding by MSAFREE2:def 11;

      SA = (SA1 +* SA2) by A1, Def4;

      then (SA . x) = (SA1 . x) & (SA1 . x) is finite or (SA . x) = (SA2 . x) & (SA2 . x) is finite by A1, A2, A4, A5, A3, A6, FUNCT_4: 13, FUNCT_4: 15;

      hence thesis;

    end;

    theorem :: CIRCCOMB:25

    for S1,S2 be non empty ManySortedSign holds for A1 be non-empty MSAlgebra over S1, s1 be Element of ( product the Sorts of A1) holds for A2 be non-empty MSAlgebra over S2, s2 be Element of ( product the Sorts of A2) st the Sorts of A1 tolerates the Sorts of A2 holds (s1 +* s2) in ( product the Sorts of (A1 +* A2))

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1;

      let s1 be Element of ( product the Sorts of A1 qua non-empty ManySortedSet of the carrier of S1);

      let A2 be non-empty MSAlgebra over S2;

      let s2 be Element of ( product the Sorts of A2 qua non-empty ManySortedSet of the carrier of S2);

      assume the Sorts of A1 tolerates the Sorts of A2;

      then the Sorts of (A1 +* A2) = (the Sorts of A1 +* the Sorts of A2) by Def4;

      hence thesis by CARD_3: 97;

    end;

    theorem :: CIRCCOMB:26

    for S1,S2 be non empty ManySortedSign holds for A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds for s be Element of ( product the Sorts of (A1 +* A2)) holds (s | the carrier of S1) in ( product the Sorts of A1) & (s | the carrier of S2) in ( product the Sorts of A2)

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1;

      let A2 be non-empty MSAlgebra over S2;

      

       A1: ( dom the Sorts of A1) = the carrier of S1 by PARTFUN1:def 2;

      

       A2: ( dom the Sorts of A2) = the carrier of S2 by PARTFUN1:def 2;

      assume

       A3: the Sorts of A1 tolerates the Sorts of A2;

      then the Sorts of (A1 +* A2) = (the Sorts of A1 +* the Sorts of A2) by Def4;

      hence thesis by A3, A1, A2, CARD_3: 98, CARD_3: 99;

    end;

    theorem :: CIRCCOMB:27

    

     Th27: for S1,S2 be non void non empty ManySortedSign holds for A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds for o be OperSymbol of (S1 +* S2), o2 be OperSymbol of S2 st o = o2 holds ( Den (o,(A1 +* A2))) = ( Den (o2,A2))

    proof

      let S1,S2 be non void non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;

      

       A1: ( dom the Charact of A2) = the carrier' of S2 by PARTFUN1:def 2;

      assume the Sorts of A1 tolerates the Sorts of A2;

      then

       A2: the Charact of (A1 +* A2) = (the Charact of A1 +* the Charact of A2) by Def4;

      let o be OperSymbol of (S1 +* S2), o2 be OperSymbol of S2;

      assume o = o2;

      hence thesis by A2, A1, FUNCT_4: 13;

    end;

    theorem :: CIRCCOMB:28

    

     Th28: for S1,S2 be non void non empty ManySortedSign holds for A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds for o be OperSymbol of (S1 +* S2), o1 be OperSymbol of S1 st o = o1 holds ( Den (o,(A1 +* A2))) = ( Den (o1,A1))

    proof

      let S1,S2 be non void non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;

      

       A1: ( dom the Charact of A1) = the carrier' of S1 by PARTFUN1:def 2;

      assume the Sorts of A1 tolerates the Sorts of A2;

      then

       A2: the Charact of (A1 +* A2) = (the Charact of A1 +* the Charact of A2) by Def4;

      assume

       A3: the Charact of A1 tolerates the Charact of A2;

      let o be OperSymbol of (S1 +* S2), o1 be OperSymbol of S1;

      assume o = o1;

      hence thesis by A2, A3, A1, FUNCT_4: 15;

    end;

    theorem :: CIRCCOMB:29

    

     Th29: for S1,S2,S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2, A be non-empty Circuit of S holds for s be State of A, s2 be State of A2 st s2 = (s | the carrier of S2) holds for g be Gate of S, g2 be Gate of S2 st g = g2 holds (g depends_on_in s) = (g2 depends_on_in s2)

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign such that

       A1: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S;

      let s be State of A, s2 be State of A2 such that

       A2: s2 = (s | the carrier of S2);

      let o be OperSymbol of S, o2 be OperSymbol of S2 such that

       A3: o = o2;

      

       A4: (the carrier of S2 |` ( the_arity_of o2)) = ( the_arity_of o2);

      

      thus (o depends_on_in s) = (s * ( the_arity_of o)) by CIRCUIT1:def 3

      .= (s * ( the_arity_of o2)) by A1, A3, Th14

      .= (s2 * ( the_arity_of o2)) by A2, A4, MONOID_1: 1

      .= (o2 depends_on_in s2) by CIRCUIT1:def 3;

    end;

    theorem :: CIRCCOMB:30

    

     Th30: for S1,S2,S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) & S1 tolerates S2 holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2, A be non-empty Circuit of S holds for s be State of A, s1 be State of A1 st s1 = (s | the carrier of S1) holds for g be Gate of S, g1 be Gate of S1 st g = g1 holds (g depends_on_in s) = (g1 depends_on_in s1)

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign such that

       A1: S = (S1 +* S2) and

       A2: S1 tolerates S2;

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S;

      let s be State of A, s1 be State of A1 such that

       A3: s1 = (s | the carrier of S1);

      let o be Gate of S, o1 be Gate of S1 such that

       A4: o = o1;

      

       A5: (the carrier of S1 |` ( the_arity_of o1)) = ( the_arity_of o1);

      

      thus (o depends_on_in s) = (s * ( the_arity_of o)) by CIRCUIT1:def 3

      .= (s * ( the_arity_of o1)) by A1, A2, A4, Th16

      .= (s1 * ( the_arity_of o1)) by A3, A5, MONOID_1: 1

      .= (o1 depends_on_in s1) by CIRCUIT1:def 3;

    end;

    theorem :: CIRCCOMB:31

    

     Th31: for S1,S2,S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, v be Vertex of S holds (for s1 be State of A1 st s1 = (s | the carrier of S1) holds v in ( InnerVertices S1) or v in the carrier of S1 & v in ( InputVertices S) implies (( Following s) . v) = (( Following s1) . v)) & (for s2 be State of A2 st s2 = (s | the carrier of S2) holds v in ( InnerVertices S2) or v in the carrier of S2 & v in ( InputVertices S) implies (( Following s) . v) = (( Following s2) . v))

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign such that

       A1: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S such that

       A2: S1 tolerates S2 and

       A3: the Sorts of A1 tolerates the Sorts of A2 and

       A4: the Charact of A1 tolerates the Charact of A2 and

       A5: A = (A1 +* A2);

      let s be State of A, v be Vertex of S;

      hereby

        let s1 be State of A1 such that

         A6: s1 = (s | the carrier of S1);

         A7:

        now

          assume v in ( InnerVertices S1);

          then

          reconsider v1 = v as Element of ( InnerVertices S1);

          

           A8: (( Following s1) . v1) = (( Den (( action_at v1),A1)) . (( action_at v1) depends_on_in s1)) by CIRCUIT2:def 5;

          v1 in ( InnerVertices S) by A1, A2, Th17;

          then

           A9: (( Following s) . v) = (( Den (( action_at v),A)) . (( action_at v) depends_on_in s)) by CIRCUIT2:def 5;

          

           A10: ( action_at v) = ( action_at v1) by A1, A2, Th17;

          then ( Den (( action_at v1),A1)) = ( Den (( action_at v),A)) by A1, A3, A4, A5, Th28;

          hence (( Following s) . v) = (( Following s1) . v) by A1, A2, A6, A10, A9, A8, Th30;

        end;

        now

          assume that

           A11: v in the carrier of S1 and

           A12: v in ( InputVertices S);

          reconsider v1 = v as Vertex of S1 by A11;

          v1 in ( InputVertices S1) by A1, A2, A12, Th13;

          then

           A13: (( Following s1) . v1) = (s1 . v1) by CIRCUIT2:def 5;

          

           A14: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

          (( Following s) . v) = (s . v) by A12, CIRCUIT2:def 5;

          hence (( Following s) . v) = (( Following s1) . v) by A6, A13, A14, FUNCT_1: 47;

        end;

        hence v in ( InnerVertices S1) or v in the carrier of S1 & v in ( InputVertices S) implies (( Following s) . v) = (( Following s1) . v) by A7;

      end;

      let s2 be State of A2 such that

       A15: s2 = (s | the carrier of S2);

       A16:

      now

        assume v in ( InnerVertices S2);

        then

        reconsider v2 = v as Element of ( InnerVertices S2);

        

         A17: (( Following s2) . v2) = (( Den (( action_at v2),A2)) . (( action_at v2) depends_on_in s2)) by CIRCUIT2:def 5;

        v2 in ( InnerVertices S) by A1, Th15;

        then

         A18: (( Following s) . v) = (( Den (( action_at v),A)) . (( action_at v) depends_on_in s)) by CIRCUIT2:def 5;

        

         A19: ( action_at v) = ( action_at v2) by A1, Th15;

        then ( Den (( action_at v2),A2)) = ( Den (( action_at v),A)) by A1, A3, A5, Th27;

        hence (( Following s) . v) = (( Following s2) . v) by A1, A15, A19, A18, A17, Th29;

      end;

      now

        assume that

         A20: v in the carrier of S2 and

         A21: v in ( InputVertices S);

        reconsider v2 = v as Vertex of S2 by A20;

        v2 in ( InputVertices S2) by A1, A21, Th12;

        then

         A22: (( Following s2) . v2) = (s2 . v2) by CIRCUIT2:def 5;

        

         A23: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

        (( Following s) . v) = (s . v) by A21, CIRCUIT2:def 5;

        hence (( Following s) . v) = (( Following s2) . v) by A15, A22, A23, FUNCT_1: 47;

      end;

      hence thesis by A16;

    end;

    theorem :: CIRCCOMB:32

    

     Th32: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) & S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, s1 be State of A1, s2 be State of A2 st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) holds ( Following s) = (( Following s1) +* ( Following s2))

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign;

      assume that

       A1: ( InnerVertices S1) misses ( InputVertices S2) and

       A2: S = (S1 +* S2);

      

       A3: the carrier of S = (the carrier of S1 \/ the carrier of S2) by A2, Def2;

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S such that

       A4: A1 tolerates A2 and

       A5: A = (A1 +* A2);

      let s be State of A, s1 be State of A1, s2 be State of A2 such that

       A6: s1 = (s | the carrier of S1) and

       A7: s2 = (s | the carrier of S2);

      

       A8: ( dom ( Following s2)) = the carrier of S2 by CIRCUIT1: 3;

      

       A9: ( dom ( Following s1)) = the carrier of S1 by CIRCUIT1: 3;

       A10:

      now

        let x be object;

        assume x in (( dom ( Following s1)) \/ ( dom ( Following s2)));

        then

        reconsider v = x as Vertex of S by A2, A9, A8, Def2;

        hereby

          assume x in ( dom ( Following s2));

          then

          reconsider v2 = x as Vertex of S2 by CIRCUIT1: 3;

           A11:

          now

            the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by A2, Def2;

            then

             A12: ( rng the ResultSort of S) c= (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2)) by FUNCT_4: 17;

            assume

             A13: v2 in ( InputVertices S2);

            then

             A14: not v2 in ( rng the ResultSort of S2) by XBOOLE_0:def 5;

             not v2 in ( rng the ResultSort of S1) by A1, A13, XBOOLE_0: 3;

            then not v in ( rng the ResultSort of S) by A14, A12, XBOOLE_0:def 3;

            hence v in ( InputVertices S) by XBOOLE_0:def 5;

          end;

          (( InputVertices S2) \/ ( InnerVertices S2)) = the carrier of S2 by XBOOLE_1: 45;

          then v2 in ( InnerVertices S2) or v2 in ( InputVertices S2) by XBOOLE_0:def 3;

          then v in ( InnerVertices S2) or v in the carrier of S2 & v in ( InputVertices S) by A11;

          hence (( Following s) . x) = (( Following s2) . x) by A2, A4, A5, A7, Th31;

        end;

        assume

         A15: not x in ( dom ( Following s2));

        then

        reconsider v1 = v as Vertex of S1 by A3, A8, XBOOLE_0:def 3;

        ( rng the ResultSort of S2) c= the carrier of S2 by RELAT_1:def 19;

        then

         A16: not v1 in ( rng the ResultSort of S2) by A8, A15;

         A17:

        now

          assume v1 in ( InputVertices S1);

          then

           A18: not v1 in ( rng the ResultSort of S1) by XBOOLE_0:def 5;

          the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by A2, Def2;

          then ( rng the ResultSort of S) c= (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2)) by FUNCT_4: 17;

          then not v in ( rng the ResultSort of S) by A16, A18, XBOOLE_0:def 3;

          hence v in ( InputVertices S) by XBOOLE_0:def 5;

        end;

        (( InputVertices S1) \/ ( InnerVertices S1)) = the carrier of S1 by XBOOLE_1: 45;

        then v1 in ( InnerVertices S1) or v1 in ( InputVertices S1) by XBOOLE_0:def 3;

        hence (( Following s) . x) = (( Following s1) . x) by A2, A4, A5, A6, A17, Th31;

      end;

      ( dom ( Following s)) = the carrier of S by CIRCUIT1: 3;

      hence thesis by A3, A9, A8, A10, FUNCT_4:def 1;

    end;

    theorem :: CIRCCOMB:33

    

     Th33: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InnerVertices S2) misses ( InputVertices S1) & S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, s1 be State of A1, s2 be State of A2 st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) holds ( Following s) = (( Following s2) +* ( Following s1))

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign such that

       A1: ( InnerVertices S2) misses ( InputVertices S1) and

       A2: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S such that

       A3: A1 tolerates A2 and

       A4: A = (A1 +* A2);

      S1 tolerates S2 by A3;

      then

       A5: S = (S2 +* S1) by A2, Th5;

      A = (A2 +* A1) by A3, A4, Th22;

      hence thesis by A1, A3, A5, Th19, Th32;

    end;

    theorem :: CIRCCOMB:34

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) c= ( InputVertices S2) & S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, s1 be State of A1, s2 be State of A2 st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) holds ( Following s) = (( Following s2) +* ( Following s1))

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign;

      assume ( InputVertices S1) c= ( InputVertices S2);

      then ( InnerVertices S2) misses ( InputVertices S1) by XBOOLE_1: 63, XBOOLE_1: 79;

      hence thesis by Th33;

    end;

    theorem :: CIRCCOMB:35

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S2) c= ( InputVertices S1) & S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, s1 be State of A1, s2 be State of A2 st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) holds ( Following s) = (( Following s1) +* ( Following s2))

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign;

      assume ( InputVertices S2) c= ( InputVertices S1);

      then ( InnerVertices S1) misses ( InputVertices S2) by XBOOLE_1: 63, XBOOLE_1: 79;

      hence thesis by Th32;

    end;

    begin

    definition

      let f be object;

      let p be FinSequence;

      let x be object;

      :: CIRCCOMB:def5

      func 1GateCircStr (p,f,x) -> non void strict ManySortedSign means

      : Def5: the carrier of it = (( rng p) \/ {x}) & the carrier' of it = { [p, f]} & (the Arity of it . [p, f]) = p & (the ResultSort of it . [p, f]) = x;

      existence

      proof

        set pf = [p, f];

        reconsider C = (( rng p) \/ {x}) as non empty set;

        x in {x} by TARSKI:def 1;

        then

        reconsider ox = x as Element of C by XBOOLE_0:def 3;

        ( rng p) c= C by XBOOLE_1: 7;

        then p is FinSequence of C by FINSEQ_1:def 4;

        then

        reconsider pp = p as Element of (C * ) by FINSEQ_1:def 11;

        reconsider R = ( {pf} --> ox) as Function of {pf}, C;

        reconsider A = ( {pf} --> pp) as Function of {pf}, (C * );

        reconsider S = ManySortedSign (# C, {pf}, A, R #) as non void strict ManySortedSign;

        take S;

        pf in {pf} by TARSKI:def 1;

        hence thesis by FUNCOP_1: 7;

      end;

      uniqueness

      proof

        let S1,S2 be non void strict ManySortedSign;

        assume

         A1: not thesis;

        then ( dom the Arity of S1) = { [p, f]} by FUNCT_2:def 1;

        then

         A2: the Arity of S1 = { [ [p, f], p]} by A1, GRFUNC_1: 7;

        ( dom the ResultSort of S1) = { [p, f]} by A1, FUNCT_2:def 1;

        then

         A3: the ResultSort of S1 = { [ [p, f], x]} by A1, GRFUNC_1: 7;

        ( dom the Arity of S2) = { [p, f]} by A1, FUNCT_2:def 1;

        then

         A4: the Arity of S2 = { [ [p, f], p]} by A1, GRFUNC_1: 7;

        ( dom the ResultSort of S2) = { [p, f]} by A1, FUNCT_2:def 1;

        hence thesis by A1, A2, A4, A3, GRFUNC_1: 7;

      end;

    end

    registration

      let f be object;

      let p be FinSequence;

      let x be object;

      cluster ( 1GateCircStr (p,f,x)) -> non empty;

      coherence

      proof

        the carrier of ( 1GateCircStr (p,f,x)) = (( rng p) \/ {x}) by Def5;

        hence the carrier of ( 1GateCircStr (p,f,x)) is non empty;

      end;

    end

    theorem :: CIRCCOMB:36

    

     Th36: for f,x be set, p be FinSequence holds the Arity of ( 1GateCircStr (p,f,x)) = ((p,f) .--> p) & the ResultSort of ( 1GateCircStr (p,f,x)) = ((p,f) .--> x)

    proof

      let f,x be set, p be FinSequence;

      set S = ( 1GateCircStr (p,f,x));

      (the Arity of S . [p, f]) = p by Def5;

      then

       A1: for x be object st x in { [p, f]} holds (the Arity of S . x) = p by TARSKI:def 1;

      

       A2: the carrier' of S = { [p, f]} by Def5;

      then ( dom the Arity of S) = { [p, f]} by FUNCT_2:def 1;

      hence the Arity of S = ((p,f) .--> p) by A1, FUNCOP_1: 11;

      (the ResultSort of S . [p, f]) = x by Def5;

      then

       A3: for y be object st y in { [p, f]} holds (the ResultSort of S . y) = x by TARSKI:def 1;

      ( dom the ResultSort of S) = { [p, f]} by A2, FUNCT_2:def 1;

      hence thesis by A3, FUNCOP_1: 11;

    end;

    theorem :: CIRCCOMB:37

    for f,x be set, p be FinSequence holds for g be Gate of ( 1GateCircStr (p,f,x)) holds g = [p, f] & ( the_arity_of g) = p & ( the_result_sort_of g) = x

    proof

      let f,x be set, p be FinSequence;

      set S = ( 1GateCircStr (p,f,x));

      let o be Gate of ( 1GateCircStr (p,f,x));

      

       A1: (the ResultSort of S . [p, f]) = x by Def5;

      

       A2: the carrier' of S = { [p, f]} by Def5;

      hence o = [p, f] by TARSKI:def 1;

      (the Arity of S . [p, f]) = p by Def5;

      hence thesis by A2, A1, TARSKI:def 1;

    end;

    theorem :: CIRCCOMB:38

    for f,x be set, p be FinSequence holds ( InputVertices ( 1GateCircStr (p,f,x))) = (( rng p) \ {x}) & ( InnerVertices ( 1GateCircStr (p,f,x))) = {x}

    proof

      let f,x be set;

      let p be FinSequence;

      the ResultSort of ( 1GateCircStr (p,f,x)) = ((p,f) .--> x) by Th36;

      then

       A1: ( rng the ResultSort of ( 1GateCircStr (p,f,x))) = {x} by FUNCOP_1: 8;

      the carrier of ( 1GateCircStr (p,f,x)) = (( rng p) \/ {x}) by Def5;

      hence thesis by A1, XBOOLE_1: 40;

    end;

    definition

      let f be object;

      let p be FinSequence;

      :: CIRCCOMB:def6

      func 1GateCircStr (p,f) -> non void strict ManySortedSign means

      : Def6: the carrier of it = (( rng p) \/ { [p, f]}) & the carrier' of it = { [p, f]} & (the Arity of it . [p, f]) = p & (the ResultSort of it . [p, f]) = [p, f];

      existence

      proof

        take ( 1GateCircStr (p,f, [p, f]));

        thus thesis by Def5;

      end;

      uniqueness

      proof

        let S1,S2 be non void strict ManySortedSign;

        assume

         A1: not thesis;

        then S1 = ( 1GateCircStr (p,f, [p, f])) by Def5;

        hence thesis by A1, Def5;

      end;

    end

    registration

      let f be object;

      let p be FinSequence;

      cluster ( 1GateCircStr (p,f)) -> non empty;

      coherence

      proof

        the carrier of ( 1GateCircStr (p,f)) = (( rng p) \/ { [p, f]}) by Def6;

        hence the carrier of ( 1GateCircStr (p,f)) is non empty;

      end;

    end

    theorem :: CIRCCOMB:39

    for f be set, p be FinSequence holds ( 1GateCircStr (p,f)) = ( 1GateCircStr (p,f, [p, f]))

    proof

      let f be set, p be FinSequence;

      set S = ( 1GateCircStr (p,f));

      

       A1: the carrier' of S = { [p, f]} by Def6;

      

       A2: (the Arity of S . [p, f]) = p by Def6;

      

       A3: (the ResultSort of S . [p, f]) = [p, f] by Def6;

      the carrier of S = (( rng p) \/ { [p, f]}) by Def6;

      hence thesis by A1, A2, A3, Def5;

    end;

    theorem :: CIRCCOMB:40

    

     Th40: for f be object, p be FinSequence holds the Arity of ( 1GateCircStr (p,f)) = ((p,f) .--> p) & the ResultSort of ( 1GateCircStr (p,f)) = ((p,f) .--> [p, f])

    proof

      let f be object, p be FinSequence;

      set S = ( 1GateCircStr (p,f));

      (the Arity of S . [p, f]) = p by Def6;

      then

       A1: for x be object st x in { [p, f]} holds (the Arity of S . x) = p by TARSKI:def 1;

      

       A2: the carrier' of S = { [p, f]} by Def6;

      then ( dom the Arity of S) = { [p, f]} by FUNCT_2:def 1;

      hence the Arity of ( 1GateCircStr (p,f)) = ((p,f) .--> p) by A1, FUNCOP_1: 11;

      (the ResultSort of S . [p, f]) = [p, f] by Def6;

      then

       A3: for x be object st x in { [p, f]} holds (the ResultSort of S . x) = [p, f] by TARSKI:def 1;

      ( dom the ResultSort of S) = { [p, f]} by A2, FUNCT_2:def 1;

      hence thesis by A3, FUNCOP_1: 11;

    end;

    theorem :: CIRCCOMB:41

    

     Th41: for f be set, p be FinSequence holds for g be Gate of ( 1GateCircStr (p,f)) holds g = [p, f] & ( the_arity_of g) = p & ( the_result_sort_of g) = g

    proof

      let f be set, p be FinSequence;

      set S = ( 1GateCircStr (p,f));

      let o be Gate of ( 1GateCircStr (p,f));

      the carrier' of S = { [p, f]} by Def6;

      hence o = [p, f] by TARSKI:def 1;

      hence thesis by Def6;

    end;

    theorem :: CIRCCOMB:42

    

     Th42: for f be object, p be FinSequence holds ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) & ( InnerVertices ( 1GateCircStr (p,f))) = { [p, f]}

    proof

      let f be object;

      let p be FinSequence;

      

       A1: the ResultSort of ( 1GateCircStr (p,f)) = ((p,f) .--> [p, f]) by Th40;

      then

       A2: ( rng the ResultSort of ( 1GateCircStr (p,f))) = { [p, f]} by FUNCOP_1: 8;

      

       A3: the carrier of ( 1GateCircStr (p,f)) = (( rng p) \/ { [p, f]}) by Def6;

      hence ( InputVertices ( 1GateCircStr (p,f))) c= ( rng p) by A2, XBOOLE_1: 43;

       A4:

      now

        assume [p, f] in ( rng p);

        then

        consider x be object such that

         A5: [x, [p, f]] in p by XTUPLE_0:def 13;

        

         A6: {x, [p, f]} in { {x, [p, f]}, {x}} by TARSKI:def 2;

        

         A7: {p, f} in { {p, f}, {p}} by TARSKI:def 2;

        

         A8: p in {p, f} by TARSKI:def 2;

         [p, f] in {x, [p, f]} by TARSKI:def 2;

        hence contradiction by A5, A8, A7, A6, XREGULAR: 9;

      end;

      thus ( rng p) c= ( InputVertices ( 1GateCircStr (p,f)))

      proof

        let x be object;

        assume

         A9: x in ( rng p);

        then

         A10: x in (( rng p) \/ { [p, f]}) by XBOOLE_0:def 3;

         not x in { [p, f]} by A4, A9, TARSKI:def 1;

        hence thesis by A2, A3, A10, XBOOLE_0:def 5;

      end;

      thus thesis by A1, FUNCOP_1: 8;

    end;

    theorem :: CIRCCOMB:43

    

     Th43: for f be set, p,q be FinSequence holds ( 1GateCircStr (p,f)) tolerates ( 1GateCircStr (q,f))

    proof

      let f be set, p,q be FinSequence;

      set S1 = ( 1GateCircStr (p,f)), S2 = ( 1GateCircStr (q,f));

      

       A1: [p, f] <> [q, f] implies { [p, f]} misses { [q, f]} by ZFMISC_1: 11;

      

       A2: the Arity of S2 = ((q,f) .--> q) by Th40;

      the Arity of S1 = ((p,f) .--> p) by Th40;

      hence the Arity of S1 tolerates the Arity of S2 by A2, A1, XTUPLE_0: 1;

      

       A3: the ResultSort of S2 = ((q,f) .--> [q, f]) by Th40;

      the ResultSort of S1 = ((p,f) .--> [p, f]) by Th40;

      hence thesis by A3, A1;

    end;

    begin

    definition

      let IT be ManySortedSign;

      :: CIRCCOMB:def7

      attr IT is unsplit means

      : Def7: the ResultSort of IT = ( id the carrier' of IT);

      :: CIRCCOMB:def8

      attr IT is gate`1=arity means

      : Def8: for g be set st g in the carrier' of IT holds g = [(the Arity of IT . g), (g `2 )];

      :: CIRCCOMB:def9

      attr IT is gate`2isBoolean means

      : Def9: for g be set st g in the carrier' of IT holds for p be FinSequence st p = (the Arity of IT . g) holds ex f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN st g = [(g `1 ), f];

    end

    definition

      let S be non empty ManySortedSign;

      let IT be MSAlgebra over S;

      :: CIRCCOMB:def10

      attr IT is gate`2=den means for g be set st g in the carrier' of S holds g = [(g `1 ), (the Charact of IT . g)];

    end

    definition

      let IT be non empty ManySortedSign;

      :: CIRCCOMB:def11

      attr IT is gate`2=den means ex A be MSAlgebra over IT st A is gate`2=den;

    end

    scheme :: CIRCCOMB:sch1

    MSSLambdaWeak { A,B() -> set , g() -> Function of A(), B() , f( object, object) -> object } :

ex f be ManySortedSet of A() st for a be set, b be Element of B() st a in A() & b = (g() . a) holds (f . a) = f(a,b);

      deffunc F( object) = f($1,.);

      consider f be Function such that

       A1: ( dom f) = A() and

       A2: for a be object st a in A() holds (f . a) = F(a) from FUNCT_1:sch 3;

      reconsider f as ManySortedSet of A() by A1, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      thus thesis by A2;

    end;

    scheme :: CIRCCOMB:sch2

    Lemma { S() -> non empty ManySortedSign , F( object, object) -> object } :

ex A be strict MSAlgebra over S() st the Sorts of A = (the carrier of S() --> BOOLEAN ) & for g be set, p be Element of (the carrier of S() * ) st g in the carrier' of S() & p = (the Arity of S() . g) holds (the Charact of A . g) = F(g,p)

      provided

       A1: for g be set, p be Element of (the carrier of S() * ) st g in the carrier' of S() & p = (the Arity of S() . g) holds F(g,p) is Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN ;

      set S = S(), SORTS = (the carrier of S --> BOOLEAN );

      consider CHARACT be ManySortedSet of the carrier' of S such that

       A2: for o be set, p be Element of (the carrier of S * ) st o in the carrier' of S & p = (the Arity of S . o) holds (CHARACT . o) = F(o,p) from MSSLambdaWeak;

      

       A3: ( dom CHARACT) = the carrier' of S by PARTFUN1:def 2;

      CHARACT is Function-yielding

      proof

        let x be object;

        assume

         A4: x in ( dom CHARACT);

        then

        reconsider o = x as Gate of S by PARTFUN1:def 2;

        reconsider p = (the Arity of S . o) as Element of (the carrier of S * ) by A3, A4, FUNCT_2: 5;

        (CHARACT . x) = F(o,p) by A2, A3, A4;

        hence thesis by A1, A3, A4;

      end;

      then

      reconsider CHARACT as ManySortedFunction of the carrier' of S;

      

       A5: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

      

       A6: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      now

        let i be object;

        assume

         A7: i in the carrier' of S;

        then

        reconsider o = i as Gate of S;

        reconsider p = (the Arity of S . o) as Element of (the carrier of S * ) by A7, FUNCT_2: 5;

        

         A8: (((SORTS # ) * the Arity of S) . i) = ((SORTS # ) . p) by A6, A7, FUNCT_1: 13;

        reconsider v = (the ResultSort of S . o) as Vertex of S by A7, FUNCT_2: 5;

        (SORTS . v) = BOOLEAN ;

        then

         A9: ((SORTS * the ResultSort of S) . i) = BOOLEAN by A5, A7, FUNCT_1: 13;

        

         A10: ((SORTS # ) . p) = (( len p) -tuples_on BOOLEAN ) by Th2;

        (CHARACT . i) = F(o,p) by A2, A7;

        hence (CHARACT . i) is Function of (((SORTS # ) * the Arity of S) . i), ((SORTS * the ResultSort of S) . i) by A1, A7, A8, A10, A9;

      end;

      then

      reconsider CHARACT as ManySortedFunction of ((SORTS # ) * the Arity of S), (SORTS * the ResultSort of S) by PBOOLE:def 15;

      take MSAlgebra (# SORTS, CHARACT #);

      thus thesis by A2;

    end;

    registration

      cluster gate`2isBoolean -> gate`2=den for non empty ManySortedSign;

      coherence

      proof

        deffunc F( object, object) = ($1 `2 );

        let S be non empty ManySortedSign;

        assume

         A1: for g be set st g in the carrier' of S holds for p be FinSequence st p = (the Arity of S . g) holds ex f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN st g = [(g `1 ), f];

         A2:

        now

          let g be set, p be Element of (the carrier of S * );

          assume that

           A3: g in the carrier' of S and

           A4: p = (the Arity of S . g);

          ex f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN st g = [(g `1 ), f] by A1, A3, A4;

          hence F(g,p) is Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN ;

        end;

        consider A be strict MSAlgebra over S such that

         A5: the Sorts of A = (the carrier of S --> BOOLEAN ) & for g be set, p be Element of (the carrier of S * ) st g in the carrier' of S & p = (the Arity of S . g) holds (the Charact of A . g) = F(g,p) from Lemma( A2);

        take A;

        let g be set;

        assume

         A6: g in the carrier' of S;

        then

        reconsider p = (the Arity of S . g) as Element of (the carrier of S * ) by FUNCT_2: 5;

        consider f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN such that

         A7: g = [(g `1 ), f] by A1, A6;

        f = (g `2 ) by A7;

        hence thesis by A5, A6, A7;

      end;

    end

    theorem :: CIRCCOMB:44

    

     Th44: for S be non empty ManySortedSign holds S is unsplit iff for o be object st o in the carrier' of S holds (the ResultSort of S . o) = o

    proof

      let S be non empty ManySortedSign;

      thus S is unsplit implies for o be object st o in the carrier' of S holds (the ResultSort of S . o) = o by FUNCT_1: 17;

      assume

       A1: for o be object st o in the carrier' of S holds (the ResultSort of S . o) = o;

      ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

      hence the ResultSort of S = ( id the carrier' of S) by A1, FUNCT_1: 17;

    end;

    theorem :: CIRCCOMB:45

    for S be non empty ManySortedSign st S is unsplit holds the carrier' of S c= the carrier of S

    proof

      let S be non empty ManySortedSign;

      assume

       A1: S is unsplit;

      let x be object;

      assume

       A2: x in the carrier' of S;

      then (the ResultSort of S . x) = x by A1, Th44;

      hence thesis by A2, FUNCT_2: 5;

    end;

    registration

      cluster unsplit -> Circuit-like for non empty ManySortedSign;

      coherence

      proof

        let S be non empty ManySortedSign such that

         A1: the ResultSort of S = ( id the carrier' of S);

        let S9 be non void non empty ManySortedSign such that

         A2: S9 = S;

        let o1,o2 be Gate of S9;

        thus thesis by A1, A2, FUNCT_1: 17;

      end;

    end

    theorem :: CIRCCOMB:46

    

     Th46: for f be object, p be FinSequence holds ( 1GateCircStr (p,f)) is unsplit gate`1=arity

    proof

      let f be object, p be FinSequence;

      set S = ( 1GateCircStr (p,f));

       A1:

      now

        let x be object;

        assume x in { [p, f]};

        then x = [p, f] by TARSKI:def 1;

        hence (the ResultSort of S . x) = x by Def6;

      end;

      

       A2: the carrier' of S = { [p, f]} by Def6;

      then ( dom the ResultSort of S) = { [p, f]} by FUNCT_2:def 1;

      hence the ResultSort of S = ( id the carrier' of S) by A2, A1, FUNCT_1: 17;

      let g be set;

      assume g in the carrier' of S;

      then

       A3: g = [p, f] by A2, TARSKI:def 1;

      then (the Arity of S . g) = p by Def6;

      hence thesis by A3;

    end;

    registration

      let f be object, p be FinSequence;

      cluster ( 1GateCircStr (p,f)) -> unsplit gate`1=arity;

      coherence by Th46;

    end

    registration

      cluster unsplit gate`1=arity non void strict non empty for ManySortedSign;

      existence

      proof

        set f = the set, p = the FinSequence;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

    end

    theorem :: CIRCCOMB:47

    

     Th47: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign holds S1 tolerates S2

    proof

      let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;

      set A1 = the Arity of S1, A2 = the Arity of S2;

      set R1 = the ResultSort of S1, R2 = the ResultSort of S2;

      thus A1 tolerates A2

      proof

        let x be object;

        assume

         A1: x in (( dom A1) /\ ( dom A2));

        then x in ( dom A2) by XBOOLE_0:def 4;

        then x in the carrier' of S2 by FUNCT_2:def 1;

        then

         A2: x = [(A2 . x), (x `2 )] by Def8;

        x in ( dom A1) by A1, XBOOLE_0:def 4;

        then x in the carrier' of S1 by FUNCT_2:def 1;

        then x = [(A1 . x), (x `2 )] by Def8;

        hence thesis by A2, XTUPLE_0: 1;

      end;

      let x be object;

      assume

       A3: x in (( dom R1) /\ ( dom R2));

      then x in ( dom R1) by XBOOLE_0:def 4;

      then x in the carrier' of S1 by FUNCT_2:def 1;

      then

       A4: (R1 . x) = x by Th44;

      x in ( dom R2) by A3, XBOOLE_0:def 4;

      then x in the carrier' of S2 by FUNCT_2:def 1;

      hence thesis by A4, Th44;

    end;

    theorem :: CIRCCOMB:48

    

     Th48: for S1,S2 be non empty ManySortedSign, A1 be MSAlgebra over S1 holds for A2 be MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den holds the Charact of A1 tolerates the Charact of A2

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 such that

       A1: A1 is gate`2=den and

       A2: A2 is gate`2=den;

      let x be object;

      set C1 = the Charact of A1, C2 = the Charact of A2;

      assume

       A3: x in (( dom C1) /\ ( dom C2));

      then x in ( dom C2) by XBOOLE_0:def 4;

      then x in the carrier' of S2 by PARTFUN1:def 2;

      then

       A4: x = [(x `1 ), (C2 . x)] by A2;

      x in ( dom C1) by A3, XBOOLE_0:def 4;

      then x in the carrier' of S1 by PARTFUN1:def 2;

      then x = [(x `1 ), (C1 . x)] by A1;

      hence thesis by A4, XTUPLE_0: 1;

    end;

    theorem :: CIRCCOMB:49

    

     Th49: for S1,S2 be unsplit non empty ManySortedSign holds (S1 +* S2) is unsplit

    proof

      let S1,S2 be unsplit non empty ManySortedSign;

      set S = (S1 +* S2);

      

       A1: the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by Def2;

      

       A2: the ResultSort of S1 = ( id the carrier' of S1) by Def7;

      

       A3: the ResultSort of S2 = ( id the carrier' of S2) by Def7;

      the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      hence the ResultSort of S = ( id the carrier' of S) by A1, A2, A3, FUNCT_4: 22;

    end;

    registration

      let S1,S2 be unsplit non empty ManySortedSign;

      cluster (S1 +* S2) -> unsplit;

      coherence by Th49;

    end

    theorem :: CIRCCOMB:50

    

     Th50: for S1,S2 be gate`1=arity non empty ManySortedSign holds (S1 +* S2) is gate`1=arity

    proof

      let S1,S2 be gate`1=arity non empty ManySortedSign;

      set S = (S1 +* S2);

      let g be set;

      

       A1: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

      

       A2: the Arity of S = (the Arity of S1 +* the Arity of S2) by Def2;

      assume

       A3: g in the carrier' of S;

      then

      reconsider g as Gate of S;

      

       A4: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

      

       A5: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      then

       A6: g in the carrier' of S1 or g in the carrier' of S2 by A3, XBOOLE_0:def 3;

       A7:

      now

        assume

         A8: not g in the carrier' of S2;

        then

        reconsider g1 = g as Gate of S1 by A5, A3, XBOOLE_0:def 3;

        

        thus g = [(the Arity of S1 . g1), (g `2 )] by A6, A8, Def8

        .= [(the Arity of S . g), (g `2 )] by A5, A2, A3, A1, A4, A8, FUNCT_4:def 1;

      end;

      now

        assume

         A9: g in the carrier' of S2;

        then

        reconsider g2 = g as Gate of S2;

        

        thus g = [(the Arity of S2 . g2), (g `2 )] by A9, Def8

        .= [(the Arity of S . g), (g `2 )] by A5, A2, A1, A4, A9, FUNCT_4:def 1;

      end;

      hence thesis by A7;

    end;

    registration

      let S1,S2 be gate`1=arity non empty ManySortedSign;

      cluster (S1 +* S2) -> gate`1=arity;

      coherence by Th50;

    end

    theorem :: CIRCCOMB:51

    

     Th51: for S1,S2 be non empty ManySortedSign st S1 is gate`2isBoolean & S2 is gate`2isBoolean holds (S1 +* S2) is gate`2isBoolean

    proof

      let S1,S2 be non empty ManySortedSign;

      set S = (S1 +* S2);

      assume that

       A1: S1 is gate`2isBoolean and

       A2: S2 is gate`2isBoolean;

      let g be set;

      assume

       A3: g in the carrier' of S;

      let p be FinSequence such that

       A4: p = (the Arity of S . g);

      reconsider g as Gate of S by A3;

      

       A5: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

      

       A6: the Arity of S = (the Arity of S1 +* the Arity of S2) by Def2;

      

       A7: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

      

       A8: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      then

       A9: g in the carrier' of S1 or g in the carrier' of S2 by A3, XBOOLE_0:def 3;

       A10:

      now

        assume

         A11: not g in the carrier' of S2;

        then

        reconsider g1 = g as Gate of S1 by A8, A3, XBOOLE_0:def 3;

        (the Arity of S1 . g1) = p by A8, A6, A3, A4, A5, A7, A11, FUNCT_4:def 1;

        hence thesis by A1, A9, A11;

      end;

      now

        assume

         A12: g in the carrier' of S2;

        then

        reconsider g2 = g as Gate of S2;

        (the Arity of S2 . g2) = p by A8, A6, A4, A5, A7, A12, FUNCT_4:def 1;

        hence thesis by A2, A12;

      end;

      hence thesis by A10;

    end;

    begin

    definition

      let n be Nat;

      mode FinSeqLen of n is n -element FinSequence;

    end

    definition

      let n be Nat;

      let X,Y be non empty set;

      let f be Function of (n -tuples_on X), Y;

      let p be FinSeqLen of n;

      let x be set;

      :: CIRCCOMB:def12

      func 1GateCircuit (p,f,x) -> strict non-empty MSAlgebra over ( 1GateCircStr (p,f,x)) means the Sorts of it = ((( rng p) --> X) +* (x .--> Y)) & (the Charact of it . [p, f]) = f;

      existence

      proof

        p is FinSequence of ( rng p) by FINSEQ_1:def 4;

        then

        reconsider p9 = p as Element of (( rng p) * ) by FINSEQ_1:def 11;

        set g1 = (( rng p) --> X), g2 = (x .--> Y);

        set S = ( 1GateCircStr (p,f,x));

        set SORTS = (g1 +* g2);

        set CHARACT = (the carrier' of S --> f);

        

         A2: ( dom (x .--> Y)) = {x};

        

         A3: x in {x} by TARSKI:def 1;

        

        then

         A4: (SORTS . x) = ((x .--> Y) . x) by A2, FUNCT_4: 13

        .= Y by A3, FUNCOP_1: 7;

        

         A5: the carrier of S = (( rng p) \/ {x}) by Def5;

        then

        reconsider SORTS as non-empty ManySortedSet of the carrier of S;

        ( rng p) c= the carrier of S by A5, XBOOLE_1: 7;

        then p is FinSequence of the carrier of S by FINSEQ_1:def 4;

        then

        reconsider pp = p as Element of (the carrier of S * ) by FINSEQ_1:def 11;

        

         A6: ( dom (g1 # )) = (( rng p) * ) by PARTFUN1:def 2;

        g1 tolerates g2

        proof

          let y be object;

          assume

           A8: y in (( dom g1) /\ ( dom g2));

          then y in ( rng p) by XBOOLE_0:def 4;

          then

           A9: (g1 . y) = X by FUNCOP_1: 7;

          

           A10: y in {x} by A8, XBOOLE_0:def 4;

          then x = y by TARSKI:def 1;

          hence thesis by A1, A8, A10, A9, FUNCOP_1: 7, XBOOLE_0:def 4;

        end;

        then g1 c= SORTS by FUNCT_4: 28;

        then (g1 # ) c= (SORTS # ) by Th1;

        then

         A11: ((g1 # ) . p9) = ((SORTS # ) . pp) by A6, GRFUNC_1: 2;

        

         A12: the carrier' of S = { [p, f]} by Def5;

        then

         A13: ( dom the ResultSort of S) = { [p, f]} by FUNCT_2:def 1;

        

         A14: (the ResultSort of S . [p, f]) = x by Def5;

        

         A15: (the Arity of S . [p, f]) = p by Def5;

        

         A16: ( len p) = n by CARD_1:def 7;

        

         A17: ( dom the Arity of S) = { [p, f]} by A12, FUNCT_2:def 1;

        now

          let i be object;

          

           A18: ((SORTS # ) . pp) = (n -tuples_on X) by A16, A11, Th2;

          assume

           A19: i in the carrier' of S;

          then

           A20: i = [p, f] by A12, TARSKI:def 1;

          then

           A21: (((SORTS # ) * the Arity of S) . i) = ((SORTS # ) . p) by A12, A15, A17, A19, FUNCT_1: 13;

          ((SORTS * the ResultSort of S) . i) = Y by A12, A14, A4, A13, A19, A20, FUNCT_1: 13;

          hence (CHARACT . i) is Function of (((SORTS # ) * the Arity of S) . i), ((SORTS * the ResultSort of S) . i) by A19, A21, A18, FUNCOP_1: 7;

        end;

        then

        reconsider CHARACT as ManySortedFunction of ((SORTS # ) * the Arity of S), (SORTS * the ResultSort of S) by PBOOLE:def 15;

        reconsider A = MSAlgebra (# SORTS, CHARACT #) as non-empty strict MSAlgebra over ( 1GateCircStr (p,f,x)) by MSUALG_1:def 3;

        take A;

         [p, f] in { [p, f]} by TARSKI:def 1;

        hence thesis by A12, FUNCOP_1: 7;

      end;

      uniqueness

      proof

        set S = ( 1GateCircStr (p,f,x));

        let A1,A2 be strict non-empty MSAlgebra over S such that

         A22: not thesis;

        

         A23: the carrier' of S = { [p, f]} by Def5;

        then ( dom the Charact of A1) = { [p, f]} by PARTFUN1:def 2;

        then

         A24: the Charact of A1 = { [ [p, f], f]} by A22, GRFUNC_1: 7;

        ( dom the Charact of A2) = { [p, f]} by A23, PARTFUN1:def 2;

        hence thesis by A22, A24, GRFUNC_1: 7;

      end;

    end

    definition

      let n be Nat;

      let X be non empty set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      :: CIRCCOMB:def13

      func 1GateCircuit (p,f) -> strict non-empty MSAlgebra over ( 1GateCircStr (p,f)) means

      : Def13: the Sorts of it = (the carrier of ( 1GateCircStr (p,f)) --> X) & (the Charact of it . [p, f]) = f;

      existence

      proof

        set S = ( 1GateCircStr (p,f));

        set SORTS = (the carrier of S --> X);

        set CHARACT = (the carrier' of S --> f);

        

         A1: ( len p) = n by CARD_1:def 7;

        

         A2: (the Arity of S . [p, f]) = p by Def6;

        

         A3: (the ResultSort of S . [p, f]) = [p, f] by Def6;

        

         A4: the carrier' of S = { [p, f]} by Def6;

        then

         A5: ( dom the ResultSort of S) = { [p, f]} by FUNCT_2:def 1;

        

         A6: the carrier of S = (( rng p) \/ { [p, f]}) by Def6;

        then ( rng p) c= the carrier of S by XBOOLE_1: 7;

        then p is FinSequence of the carrier of S by FINSEQ_1:def 4;

        then

        reconsider pp = p as Element of (the carrier of S * ) by FINSEQ_1:def 11;

        

         A7: [p, f] in { [p, f]} by TARSKI:def 1;

        then [p, f] in the carrier of S by A6, XBOOLE_0:def 3;

        then

         A8: (SORTS . [p, f]) = X by FUNCOP_1: 7;

        

         A9: ( dom the Arity of S) = { [p, f]} by A4, FUNCT_2:def 1;

        now

          let i be object;

          

           A10: ((SORTS # ) . pp) = (n -tuples_on X) by A1, Th2;

          assume

           A11: i in the carrier' of S;

          then

           A12: i = [p, f] by A4, TARSKI:def 1;

          then

           A13: (((SORTS # ) * the Arity of S) . i) = ((SORTS # ) . p) by A4, A2, A9, A11, FUNCT_1: 13;

          ((SORTS * the ResultSort of S) . i) = X by A4, A3, A8, A5, A11, A12, FUNCT_1: 13;

          hence (CHARACT . i) is Function of (((SORTS # ) * the Arity of S) . i), ((SORTS * the ResultSort of S) . i) by A11, A13, A10, FUNCOP_1: 7;

        end;

        then

        reconsider CHARACT as ManySortedFunction of ((SORTS # ) * the Arity of S), (SORTS * the ResultSort of S) by PBOOLE:def 15;

        reconsider A = MSAlgebra (# SORTS, CHARACT #) as non-empty strict MSAlgebra over ( 1GateCircStr (p,f)) by MSUALG_1:def 3;

        take A;

        thus thesis by A4, A7, FUNCOP_1: 7;

      end;

      uniqueness

      proof

        set S = ( 1GateCircStr (p,f));

        let A1,A2 be strict non-empty MSAlgebra over S such that

         A14: not thesis;

        

         A15: the carrier' of S = { [p, f]} by Def6;

        then ( dom the Charact of A1) = { [p, f]} by PARTFUN1:def 2;

        then

         A16: the Charact of A1 = { [ [p, f], f]} by A14, GRFUNC_1: 7;

        ( dom the Charact of A2) = { [p, f]} by A15, PARTFUN1:def 2;

        hence thesis by A14, A16, GRFUNC_1: 7;

      end;

    end

    theorem :: CIRCCOMB:52

    

     Th52: for n be Nat, X be non empty set holds for f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds ( 1GateCircuit (p,f)) is gate`2=den & ( 1GateCircStr (p,f)) is gate`2=den

    proof

      let n be Nat;

      let X be non empty set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      thus

       A1: ( 1GateCircuit (p,f)) is gate`2=den

      proof

        let g be set;

        assume g in the carrier' of ( 1GateCircStr (p,f));

        then

         A2: g = [p, f] by Th41;

        

        hence g = [(g `1 ), f]

        .= [(g `1 ), (the Charact of ( 1GateCircuit (p,f)) . g)] by A2, Def13;

      end;

      take ( 1GateCircuit (p,f));

      thus thesis by A1;

    end;

    registration

      let n be Nat, X be non empty set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      cluster ( 1GateCircuit (p,f)) -> gate`2=den;

      coherence by Th52;

      cluster ( 1GateCircStr (p,f)) -> gate`2=den;

      coherence by Th52;

    end

    theorem :: CIRCCOMB:53

    

     Th53: for n be Nat holds for p be FinSeqLen of n holds for f be Function of (n -tuples_on BOOLEAN ), BOOLEAN holds ( 1GateCircStr (p,f)) is gate`2isBoolean

    proof

      set X = BOOLEAN ;

      let n be Nat;

      let p be FinSeqLen of n;

      let f be Function of (n -tuples_on X), X;

      let g be set;

      

       A1: ( len p) = n by CARD_1:def 7;

      

       A2: (the Arity of ( 1GateCircStr (p,f)) . [p, f]) = p by Def6;

      assume g in the carrier' of ( 1GateCircStr (p,f));

      then

       A3: g = [p, f] by Th41;

      let q be FinSequence;

      assume q = (the Arity of ( 1GateCircStr (p,f)) . g);

      then

      reconsider f as Function of (( len q) -tuples_on X), X by A3, A2, A1;

      take f;

      thus thesis by A3;

    end;

    registration

      let n be Nat;

      let f be Function of (n -tuples_on BOOLEAN ), BOOLEAN ;

      let p be FinSeqLen of n;

      cluster ( 1GateCircStr (p,f)) -> gate`2isBoolean;

      coherence by Th53;

    end

    registration

      cluster gate`2isBoolean non empty for ManySortedSign;

      existence

      proof

        set p = the FinSeqLen of 0 ;

        set f = the Function of ( 0 -tuples_on BOOLEAN ), BOOLEAN ;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

    end

    registration

      let S1,S2 be gate`2isBoolean non empty ManySortedSign;

      cluster (S1 +* S2) -> gate`2isBoolean;

      coherence by Th51;

    end

    theorem :: CIRCCOMB:54

    

     Th54: for n be Nat, X be non empty set, f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds the Charact of ( 1GateCircuit (p,f)) = ((p,f) .--> f) & for v be Vertex of ( 1GateCircStr (p,f)) holds (the Sorts of ( 1GateCircuit (p,f)) . v) = X

    proof

      let n be Nat, X be non empty set, f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      set S = ( 1GateCircStr (p,f)), A = ( 1GateCircuit (p,f));

      (the Charact of A . [p, f]) = f by Def13;

      then

       A1: for x be object st x in { [p, f]} holds (the Charact of A . x) = f by TARSKI:def 1;

      the carrier' of S = { [p, f]} by Def6;

      then ( dom the Charact of A) = { [p, f]} by PARTFUN1:def 2;

      hence the Charact of A = ((p,f) .--> f) by A1, FUNCOP_1: 11;

      let v be Vertex of S;

      the Sorts of A = (the carrier of S --> X) by Def13;

      hence thesis;

    end;

    registration

      let n be Nat;

      let X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      cluster ( 1GateCircuit (p,f)) -> finite-yielding;

      coherence

      proof

        let i be object;

        set S = ( 1GateCircStr (p,f));

        assume i in the carrier of S;

        hence thesis by Th54;

      end;

    end

    theorem :: CIRCCOMB:55

    for n be Nat, X be non empty set, f be Function of (n -tuples_on X), X, p,q be FinSeqLen of n holds ( 1GateCircuit (p,f)) tolerates ( 1GateCircuit (q,f))

    proof

      let n be Nat, X be non empty set, f be Function of (n -tuples_on X), X;

      let p,q be FinSeqLen of n;

      set S1 = ( 1GateCircStr (p,f)), S2 = ( 1GateCircStr (q,f));

      set A1 = ( 1GateCircuit (p,f)), A2 = ( 1GateCircuit (q,f));

      thus ( 1GateCircStr (p,f)) tolerates ( 1GateCircStr (q,f)) by Th43;

      

       A1: the Sorts of A2 = (the carrier of S2 --> X) by Def13;

      the Sorts of A1 = (the carrier of S1 --> X) by Def13;

      hence the Sorts of A1 tolerates the Sorts of A2 by A1, FUNCOP_1: 87;

      

       A2: the Charact of A2 = ((q,f) .--> f) by Th54;

      the Charact of A1 = ((p,f) .--> f) by Th54;

      hence thesis by A2, FUNCOP_1: 87;

    end;

    theorem :: CIRCCOMB:56

    for n be Nat, X be finite non empty set, f be Function of (n -tuples_on X), X, p be FinSeqLen of n holds for s be State of ( 1GateCircuit (p,f)) holds (( Following s) . [p, f]) = (f . (s * p))

    proof

      let n be Nat;

      let X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      let s be State of ( 1GateCircuit (p,f));

      set S = ( 1GateCircStr (p,f)), A = ( 1GateCircuit (p,f));

      set IV = ( InnerVertices S);

      IV = { [p, f]} by Th42;

      then

      reconsider v = [p, f] as Element of IV by TARSKI:def 1;

      the carrier' of S = { [p, f]} by Def6;

      then

      reconsider o = [p, f] as Gate of S by TARSKI:def 1;

      ( the_result_sort_of o) = v by Def6;

      then

       A1: ( action_at v) = o by MSAFREE2:def 7;

      ( the_arity_of o) = p by Def6;

      then

       A2: (o depends_on_in s) = (s * p) by CIRCUIT1:def 3;

      (( Following s) . v) = (( Den (( action_at v),A)) . (( action_at v) depends_on_in s)) by CIRCUIT2:def 5;

      hence thesis by A1, A2, Def13;

    end;

    begin

    definition

      let S be non empty ManySortedSign;

      let IT be MSAlgebra over S;

      :: CIRCCOMB:def14

      attr IT is Boolean means for v be Vertex of S holds (the Sorts of IT . v) = BOOLEAN ;

    end

    theorem :: CIRCCOMB:57

    

     Th57: for S be non empty ManySortedSign, A be MSAlgebra over S holds A is Boolean iff the Sorts of A = (the carrier of S --> BOOLEAN )

    proof

      let S be non empty ManySortedSign, A be MSAlgebra over S;

      

       A1: ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      thus A is Boolean implies the Sorts of A = (the carrier of S --> BOOLEAN )

      proof

        assume for v be Vertex of S holds (the Sorts of A . v) = BOOLEAN ;

        then for v be object st v in the carrier of S holds (the Sorts of A . v) = BOOLEAN ;

        hence thesis by A1, FUNCOP_1: 11;

      end;

      assume

       A2: the Sorts of A = (the carrier of S --> BOOLEAN );

      let v be Vertex of S;

      thus thesis by A2;

    end;

    registration

      let S be non empty ManySortedSign;

      cluster Boolean -> non-empty finite-yielding for MSAlgebra over S;

      coherence

      proof

        let A be MSAlgebra over S;

        assume

         A1: A is Boolean;

        then the Sorts of A = (the carrier of S --> BOOLEAN ) by Th57;

        hence A is non-empty;

        let v be object;

        thus thesis by A1;

      end;

    end

    theorem :: CIRCCOMB:58

    for S be non empty ManySortedSign, A be MSAlgebra over S holds A is Boolean iff ( rng the Sorts of A) c= { BOOLEAN }

    proof

      let S be non empty ManySortedSign, A be MSAlgebra over S;

      hereby

        assume A is Boolean;

        then the Sorts of A = (the carrier of S --> BOOLEAN ) by Th57;

        hence ( rng the Sorts of A) c= { BOOLEAN } by FUNCOP_1: 13;

      end;

      assume

       A1: ( rng the Sorts of A) c= { BOOLEAN };

      let v be Vertex of S;

      ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      then (the Sorts of A . v) in ( rng the Sorts of A) by FUNCT_1:def 3;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: CIRCCOMB:59

    

     Th59: for S1,S2 be non empty ManySortedSign holds for A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds the Sorts of A1 tolerates the Sorts of A2

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2;

      assume that

       A1: A1 is Boolean and

       A2: A2 is Boolean;

      

       A3: the Sorts of A2 = (the carrier of S2 --> BOOLEAN ) by A2, Th57;

      the Sorts of A1 = (the carrier of S1 --> BOOLEAN ) by A1, Th57;

      hence thesis by A3, FUNCOP_1: 87;

    end;

    theorem :: CIRCCOMB:60

    

     Th60: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign holds for A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 is Boolean gate`2=den & A2 is Boolean gate`2=den holds A1 tolerates A2 by Th47, Th48, Th59;

    registration

      let S be non empty ManySortedSign;

      cluster Boolean for strict MSAlgebra over S;

      existence

      proof

        deffunc F( set, Element of (the carrier of S * )) = ((( len $2) -tuples_on BOOLEAN ) --> FALSE );

        

         A1: for g be set, p be Element of (the carrier of S * ) st g in the carrier' of S & p = (the Arity of S . g) holds F(g,p) is Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN ;

        consider A be strict MSAlgebra over S such that

         A2: the Sorts of A = (the carrier of S --> BOOLEAN ) & for g be set, p be Element of (the carrier of S * ) st g in the carrier' of S & p = (the Arity of S . g) holds (the Charact of A . g) = F(g,p) from Lemma( A1);

        take A;

        let v be Vertex of S;

        thus thesis by A2;

      end;

    end

    theorem :: CIRCCOMB:61

    for n be Nat, f be Function of (n -tuples_on BOOLEAN ), BOOLEAN holds for p be FinSeqLen of n holds ( 1GateCircuit (p,f)) is Boolean

    proof

      let n be Nat, f be Function of (n -tuples_on BOOLEAN ), BOOLEAN ;

      let p be FinSeqLen of n;

      set S = ( 1GateCircStr (p,f)), A = ( 1GateCircuit (p,f));

      let v be Vertex of S;

      the Sorts of A = (the carrier of S --> BOOLEAN ) by Def13;

      hence thesis;

    end;

    theorem :: CIRCCOMB:62

    

     Th62: for S1,S2 be non empty ManySortedSign holds for A1 be Boolean MSAlgebra over S1 holds for A2 be Boolean MSAlgebra over S2 holds (A1 +* A2) is Boolean

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be Boolean MSAlgebra over S1;

      let A2 be Boolean MSAlgebra over S2;

      set A = (A1 +* A2);

      set S = (S1 +* S2);

      let x be Vertex of S;

      the carrier of S = (the carrier of S1 \/ the carrier of S2) by Def2;

      then

       A3: x in the carrier of S1 or x in the carrier of S2 by XBOOLE_0:def 3;

      

       A4: the Sorts of A2 = (the carrier of S2 --> BOOLEAN ) by Th57;

      

       A5: the Sorts of A1 = (the carrier of S1 --> BOOLEAN ) by Th57;

      then

       A6: the Sorts of A1 tolerates the Sorts of A2 by A4, FUNCOP_1: 87;

      then the Sorts of A = (the Sorts of A1 +* the Sorts of A2) by Def4;

      then (the Sorts of A . x) = (the Sorts of A1 . x) & (the Sorts of A1 . x) = BOOLEAN or (the Sorts of A . x) = (the Sorts of A2 . x) & (the Sorts of A2 . x) = BOOLEAN by A5, A4, A6, A3, FUNCOP_1: 7, FUNCT_4: 13, FUNCT_4: 15;

      hence thesis;

    end;

    theorem :: CIRCCOMB:63

    

     Th63: for S1,S2 be non empty ManySortedSign holds for A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds (A1 +* A2) is gate`2=den

    proof

      let S1,S2 be non empty ManySortedSign;

      let A1 be non-empty MSAlgebra over S1;

      let A2 be non-empty MSAlgebra over S2;

      set A = (A1 +* A2);

      set S = (S1 +* S2);

      assume that

       A1: A1 is gate`2=den and

       A2: A2 is gate`2=den and

       A3: the Sorts of A1 tolerates the Sorts of A2;

      

       A4: the Charact of A = (the Charact of A1 +* the Charact of A2) by A3, Def4;

      let g be set;

      

       A5: ( dom the Charact of A1) = the carrier' of S1 by PARTFUN1:def 2;

      

       A6: ( dom the Charact of A2) = the carrier' of S2 by PARTFUN1:def 2;

      

       A7: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by Def2;

      assume g in the carrier' of S;

      then

       A8: g in the carrier' of S1 or g in the carrier' of S2 by A7, XBOOLE_0:def 3;

      the Charact of A1 tolerates the Charact of A2 by A1, A2, Th48;

      then (the Charact of A . g) = (the Charact of A1 . g) & [(g `1 ), (the Charact of A1 . g)] = g or (the Charact of A . g) = (the Charact of A2 . g) & [(g `1 ), (the Charact of A2 . g)] = g by A1, A2, A4, A5, A6, A8, FUNCT_4: 13, FUNCT_4: 15;

      hence thesis;

    end;

    registration

      cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void strict for non empty ManySortedSign;

      existence

      proof

        set p = the FinSeqLen of 1;

        set f = the Function of (1 -tuples_on BOOLEAN ), BOOLEAN ;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

    end

    registration

      let S be gate`2isBoolean non empty ManySortedSign;

      cluster Boolean gate`2=den for strict MSAlgebra over S;

      existence

      proof

        deffunc F( set, set) = ($1 `2 );

         A1:

        now

          let g be set, p be Element of (the carrier of S * );

          assume that

           A2: g in the carrier' of S and

           A3: p = (the Arity of S . g);

          ex f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN st g = [(g `1 ), f] by A2, A3, Def9;

          hence F(g,p) is Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN ;

        end;

        consider A be strict MSAlgebra over S such that

         A4: the Sorts of A = (the carrier of S --> BOOLEAN ) & for g be set, p be Element of (the carrier of S * ) st g in the carrier' of S & p = (the Arity of S . g) holds (the Charact of A . g) = F(g,p) from Lemma( A1);

        take A;

        thus A is Boolean by A4;

        let g be set;

        assume

         A5: g in the carrier' of S;

        then

        reconsider p = (the Arity of S . g) as Element of (the carrier of S * ) by FUNCT_2: 5;

        consider f be Function of (( len p) -tuples_on BOOLEAN ), BOOLEAN such that

         A6: g = [(g `1 ), f] by A5, Def9;

        (g `2 ) = f by A6;

        hence thesis by A4, A5, A6;

      end;

    end

    registration

      let S1,S2 be unsplit gate`2isBoolean non void non empty ManySortedSign;

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      cluster (A1 +* A2) -> Boolean gate`2=den;

      coherence

      proof

        the Sorts of A1 tolerates the Sorts of A2 by Th59;

        hence thesis by Th62, Th63;

      end;

    end

    registration

      let n be Nat;

      let X be finite non empty set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      cluster gate`2=den strict non-empty for Circuit of ( 1GateCircStr (p,f));

      existence

      proof

        take ( 1GateCircuit (p,f));

        thus thesis;

      end;

    end

    registration

      let n be Nat;

      let X be finite non empty set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      cluster ( 1GateCircuit (p,f)) -> gate`2=den;

      coherence ;

    end

    theorem :: CIRCCOMB:64

    for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), v be Vertex of (S1 +* S2) holds (for s1 be State of A1 st s1 = (s | the carrier of S1) holds v in ( InnerVertices S1) or v in the carrier of S1 & v in ( InputVertices (S1 +* S2)) implies (( Following s) . v) = (( Following s1) . v)) & for s2 be State of A2 st s2 = (s | the carrier of S2) holds v in ( InnerVertices S2) or v in the carrier of S2 & v in ( InputVertices (S1 +* S2)) implies (( Following s) . v) = (( Following s2) . v)

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign;

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      A1 tolerates A2 by Th60;

      hence thesis by Th31;

    end;