facirc_2.miz

    begin

    theorem :: FACIRC_2:1



     Th1: for x,y,z be set st x <> z & y <> z holds ( {x, y} \ {z}) = {x, y}

    proof

      let x,y,z be set;

      assume that

       A1: x <> z and

       A2: y <> z;

      for a be object st a in {x, y} holds not a in {z}

      proof

        let a be object;

        assume a in {x, y};

        then a <> z by A1, A2, TARSKI:def 2;

        hence thesis by TARSKI:def 1;

      end;

      then {x, y} misses {z} by XBOOLE_0: 3;

      hence thesis by XBOOLE_1: 83;

    end;

    theorem :: FACIRC_2:2

    for x,y,z be set holds x <> [ <*x, y*>, z] & y <> [ <*x, y*>, z]

    proof

      let x,y,z be set;



       A1: ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      then

       A2: x in ( rng <*x, y*>) by TARSKI:def 2;



       A3: y in ( rng <*x, y*>) by A1, TARSKI:def 2;



       A4: ( the_rank_of x) in ( the_rank_of [ <*x, y*>, z]) by A2, CLASSES1: 82;

      ( the_rank_of y) in ( the_rank_of [ <*x, y*>, z]) by A3, CLASSES1: 82;

      hence thesis by A4;

    end;

    registration

      cluster void -> unsplit gate`1=arity gate`2isBoolean for ManySortedSign;

      coherence

      proof

        let S be ManySortedSign;

        assume

         A1: the carrier' of S is empty;



        hence the ResultSort of S = {}

        .= ( id the carrier' of S) by A1;

        thus S is gate`1=arity by A1;

        let g be set;

        thus thesis by A1;

      end;

    end

    registration

      cluster strict void for ManySortedSign;

      existence

      proof

        set S = the strict void ManySortedSign;

        take S;

        thus thesis;

      end;

    end

    definition

      let x be set;

      :: FACIRC_2:def1

      func SingleMSS (x) -> strict void ManySortedSign means

      : Def1: the carrier of it = {x};

      existence

      proof

        set a = the Function of {} , ( {x} * );

        set r = the Function of {} , {x};

        reconsider S = ManySortedSign (# {x}, {} , a, r #) as void strict ManySortedSign;

        take S;

        thus thesis;

      end;

      uniqueness

      proof

        let S1,S2 be strict void ManySortedSign such that

         A1: the carrier of S1 = {x} and

         A2: the carrier of S2 = {x};

        the Arity of S1 = the Arity of S2;

        hence thesis by A1, A2;

      end;

    end

    registration

      let x be set;

      cluster ( SingleMSS x) -> non empty;

      coherence

      proof

        the carrier of ( SingleMSS x) = {x} by Def1;

        hence the carrier of ( SingleMSS x) is non empty;

      end;

    end

    definition

      let x be set;

      :: FACIRC_2:def2

      func SingleMSA (x) -> Boolean strict MSAlgebra over ( SingleMSS x) means not contradiction;

      existence ;

      uniqueness

      proof

        set S = ( SingleMSS x);

        let A1,A2 be Boolean strict MSAlgebra over S;



         A1: the Sorts of A1 = (the carrier of S --> BOOLEAN ) by CIRCCOMB: 57;



         A2: the Charact of A1 = {} ;

        the Charact of A2 = {} ;

        hence thesis by A1, A2, CIRCCOMB: 57;

      end;

    end

    theorem :: FACIRC_2:3

    for x be set, S be ManySortedSign holds ( SingleMSS x) tolerates S by PARTFUN1: 59;

    theorem :: FACIRC_2:4



     Th4: for x be set, S be non empty ManySortedSign st x in the carrier of S holds (( SingleMSS x) +* S) = the ManySortedSign of S

    proof

      let x be set, S be non empty ManySortedSign;

      set T = (( SingleMSS x) +* S);

      assume x in the carrier of S;

      then {x} c= the carrier of S by ZFMISC_1: 31;

      then

       A1: ( {x} \/ the carrier of S) = the carrier of S by XBOOLE_1: 12;



       A2: ( {} \/ the carrier' of S) = the carrier' of S;



       A3: the carrier of ( SingleMSS x) = {x} by Def1;



       A4: the ResultSort of ( SingleMSS x) = {} ;



       A5: the Arity of ( SingleMSS x) = {} ;



       A6: ( {} +* the ResultSort of S) = the ResultSort of S;



       A7: ( {} +* the Arity of S) = the Arity of S;



       A8: the carrier of T = the carrier of S by A1, A3, CIRCCOMB:def 2;



       A9: the carrier' of T = the carrier' of S by A2, A4, CIRCCOMB:def 2;

      the ResultSort of T = the ResultSort of S by A4, A6, CIRCCOMB:def 2;

      hence thesis by A5, A7, A8, A9, CIRCCOMB:def 2;

    end;

    theorem :: FACIRC_2:5

    for x be set, S be non empty strict ManySortedSign holds for A be Boolean MSAlgebra over S st x in the carrier of S holds (( SingleMSA x) +* A) = the MSAlgebra of A

    proof

      let x be set, S be non empty strict ManySortedSign;

      let A be Boolean MSAlgebra over S;

      set S1 = ( SingleMSS x), A1 = ( SingleMSA x);

      assume

       A1: x in the carrier of S;

      then

       A2: (S1 +* S) = S by Th4;



       A3: {x} c= the carrier of S by A1, ZFMISC_1: 31;



       A4: the carrier of S1 = {x} by Def1;



       A5: the Sorts of A = (the carrier of S --> BOOLEAN ) by CIRCCOMB: 57;

      the Sorts of A1 = (the carrier of S1 --> BOOLEAN ) by CIRCCOMB: 57;

      then

       A6: the Sorts of A1 tolerates the Sorts of A by A5, FUNCOP_1: 87;



       A7: the Charact of A = (the Charact of A1 +* the Charact of A);



       A8: the Sorts of (A1 +* A) = (the Sorts of A1 +* the Sorts of A) by A6, CIRCCOMB:def 4;



       A9: the Charact of A = the Charact of (A1 +* A) by A6, A7, CIRCCOMB:def 4;



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

      ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      hence thesis by A2, A3, A4, A8, A9, A10, FUNCT_4: 19;

    end;

    notation

      synonym <*> for {} ;

    end

    definition

      let n be Nat;

      let x,y be FinSequence;



       A1: ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) is unsplit gate`1=arity gate`2isBoolean non void non empty strict;

      :: FACIRC_2:def3

      func n -BitAdderStr (x,y) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign means

      : Def3: ex f,g be ManySortedSet of NAT st it = (f . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (g . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, z be set st S = (f . n) & z = (g . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z));

      uniqueness

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

        for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2 from CIRCCMB2:sch 9;

        hence thesis;

      end;

      existence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        deffunc S( set, Nat) = ( BitAdderWithOverflowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        ex S be unsplit gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = (S +* S(x,n)) & (h . (n + 1)) = o(x,n) from CIRCCMB2:sch 8( A1);

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      let x,y be FinSequence;

      :: FACIRC_2:def4

      func n -BitAdderCirc (x,y) -> Boolean gate`2=den strict Circuit of (n -BitAdderStr (x,y)) means

      : Def4: ex f,g,h be ManySortedSet of NAT st (n -BitAdderStr (x,y)) = (f . n) & it = (g . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z));

      uniqueness

      proof

        set S0 = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

        set A0 = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

        set Sn = (n -BitAdderStr (x,y));

        set o0 = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

        deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

        deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitAdderWithOverflowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3)));



         A1: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set, n be Nat holds A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);

        thus for A1,A2 be Boolean gate`2=den strict Circuit of (n -BitAdderStr (x,y)) st (ex f,g,h be ManySortedSet of NAT st Sn = (f . n) & A1 = (g . n) & (f . 0 ) = S0 & (g . 0 ) = A0 & (h . 0 ) = o0 & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,g,h be ManySortedSet of NAT st Sn = (f . n) & A2 = (g . n) & (f . 0 ) = S0 & (g . 0 ) = A0 & (h . 0 ) = o0 & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) holds A1 = A2 from CIRCCMB2:sch 21( A1);

      end;

      existence

      proof

        set S0 = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

        set A0 = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

        set Sn = (n -BitAdderStr (x,y));

        set o0 = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

        deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

        deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitAdderWithOverflowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3)));



         A2: for S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, z be set, n be Nat holds S(S,z,n) is unsplit gate`1=arity gate`2isBoolean non void strict;



         A3: for S,S1 be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A be Boolean gate`2=den strict Circuit of S holds for z be set, n be Nat st S1 = S(S,z,n) holds A(S,A,z,n) is Boolean gate`2=den strict Circuit of S1;



         A4: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set, n be Nat holds A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);



         A5: ex f,h be ManySortedSet of NAT st Sn = (f . n) & (f . 0 ) = S0 & (h . 0 ) = o0 & for n be Nat, S be non empty ManySortedSign, z be set st S = (f . n) & z = (h . n) holds (f . (n + 1)) = S(S,z,n) & (h . (n + 1)) = o(z,n) by Def3;

        thus ex A be Boolean gate`2=den strict Circuit of Sn, f,g,h be ManySortedSet of NAT st Sn = (f . n) & A = (g . n) & (f . 0 ) = S0 & (g . 0 ) = A0 & (h . 0 ) = o0 & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB2:sch 19( A2, A5, A4, A3);

      end;

    end

    definition

      let n be Nat;

      let x,y be FinSequence;

      set c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

      :: FACIRC_2:def5

      func n -BitMajorityOutput (x,y) -> Element of ( InnerVertices (n -BitAdderStr (x,y))) means

      : Def5: ex h be ManySortedSet of NAT st it = (h . n) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, z be set st z = (h . n) holds (h . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z));

      uniqueness

      proof

        let o1,o2 be Element of ( InnerVertices (n -BitAdderStr (x,y)));

        given h1 be ManySortedSet of NAT such that

         A1: o1 = (h1 . n) and

         A2: (h1 . 0 ) = c and

         A3: for n be Nat, z be set st z = (h1 . n) holds (h1 . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z));

        given h2 be ManySortedSet of NAT such that

         A4: o2 = (h2 . n) and

         A5: (h2 . 0 ) = c and

         A6: for n be Nat, z be set st z = (h2 . n) holds (h2 . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z));

        deffunc F( Nat, set) = ( MajorityOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2));



         A7: ( dom h1) = NAT by PARTFUN1:def 2;



         A8: (h1 . 0 ) = c by A2;



         A9: for n be Nat holds (h1 . (n + 1)) = F(n,.) by A3;



         A10: ( dom h2) = NAT by PARTFUN1:def 2;



         A11: (h2 . 0 ) = c by A5;



         A12: for n be Nat holds (h2 . (n + 1)) = F(n,.) by A6;

        h1 = h2 from NAT_1:sch 15( A7, A8, A9, A10, A11, A12);

        hence thesis by A1, A4;

      end;

      existence

      proof

        defpred P[ set, set, set] means not contradiction;

        deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

        deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

        consider f,g be ManySortedSet of NAT such that

         A13: (n -BitAdderStr (x,y)) = (f . n) and

         A14: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

         A15: (g . 0 ) = c and

         A16: for n be Nat, S be non empty ManySortedSign, z be set st S = (f . n) & z = (g . n) holds (f . (n + 1)) = S(S,z,n) & (g . (n + 1)) = o(z,n) by Def3;

        defpred P[ Nat] means ex S be non empty ManySortedSign st S = (f . $1) & (g . $1) in ( InnerVertices S);

        ( InnerVertices ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )))) = {c} by CIRCCOMB: 42;

        then c in ( InnerVertices ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )))) by TARSKI:def 1;

        then

         A17: P[ 0 ] by A14, A15;



         A18: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat such that

           A19: ex S be non empty ManySortedSign st S = (f . i) & (g . i) in ( InnerVertices S) and

           A20: for S be non empty ManySortedSign st S = (f . (i + 1)) holds not (g . (i + 1)) in ( InnerVertices S);

          consider S be non empty ManySortedSign such that

           A21: S = (f . i) and (g . i) in ( InnerVertices S) by A19;

          ( MajorityOutput ((x . (i + 1)),(y . (i + 1)),(g . i))) in ( InnerVertices ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(g . i)))) by FACIRC_1: 90;

          then

           A22: ( MajorityOutput ((x . (i + 1)),(y . (i + 1)),(g . i))) in ( InnerVertices (S +* ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(g . i))))) by FACIRC_1: 22;



           A23: (f . (i + 1)) = (S +* ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(g . i)))) by A16, A21;

          (g . (i + 1)) = ( MajorityOutput ((x . (i + 1)),(y . (i + 1)),(g . i))) by A16, A21;

          hence contradiction by A20, A22, A23;

        end;

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        for i be Nat holds P[i] from NAT_1:sch 2( A17, A18);

        then ex S be non empty ManySortedSign st S = (f . n9) & (g . n) in ( InnerVertices S);

        then

        reconsider o = (g . n9) as Element of ( InnerVertices (n -BitAdderStr (x,y))) by A13;

        take o, g;

        thus o = (g . n) & (g . 0 ) = c by A15;

        let i be Nat;



         A24: ex S be non empty ManySortedSign, x be set st S = (f . 0 ) & x = (g . 0 ) & P[S, x, 0 ] by A14;



         A25: for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (g . n) & P[S, x, n] holds P[ S(S,x,n), o(x,n), (n + 1)];

        for n be Nat holds ex S be non empty ManySortedSign st S = (f . n) & P[S, (g . n), n] from CIRCCMB2:sch 2( A24, A16, A25);

        then ex S be non empty ManySortedSign st S = (f . i);

        hence thesis by A16;

      end;

    end

    theorem :: FACIRC_2:6



     Th6: for x,y be FinSequence, f,g,h be ManySortedSet of NAT st (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)) holds for n be Nat holds (n -BitAdderStr (x,y)) = (f . n) & (n -BitAdderCirc (x,y)) = (g . n) & (n -BitMajorityOutput (x,y)) = (h . n)

    proof

      let x,y be FinSequence, f,g,h be ManySortedSet of NAT ;

      deffunc o( set, Nat) = ( MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1));

      deffunc F( Nat, set) = ( MajorityOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2));

      deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

      deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitAdderWithOverflowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3)));

      assume that

       A1: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A2: (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] and

       A3: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = S(S,z,n) & (g . (n + 1)) = A(S,A,z,n) & (h . (n + 1)) = o(z,n);

      let n be Nat;

      consider f1,g1,h1 be ManySortedSet of NAT such that

       A4: (n -BitAdderStr (x,y)) = (f1 . n) and

       A5: (n -BitAdderCirc (x,y)) = (g1 . n) and

       A6: (f1 . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A7: (g1 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A8: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] and

       A9: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f1 . n) & A = (g1 . n) & z = (h1 . n) holds (f1 . (n + 1)) = S(S,z,n) & (g1 . (n + 1)) = A(S,A,z,n) & (h1 . (n + 1)) = o(z,n) by Def4;



       A10: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . 0 ) & A = (g . 0 ) by A1;



       A11: (f . 0 ) = (f1 . 0 ) & (g . 0 ) = (g1 . 0 ) & (h . 0 ) = (h1 . 0 ) by A1, A2, A6, A7, A8;



       A12: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set, n be Nat holds A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);

      f = f1 & g = g1 & h = h1 from CIRCCMB2:sch 14( A10, A11, A3, A9, A12);

      hence (n -BitAdderStr (x,y)) = (f . n) & (n -BitAdderCirc (x,y)) = (g . n) by A4, A5;



       A13: for n be Nat, S be non empty ManySortedSign, z be set st S = (f . n) & z = (h . n) holds (f . (n + 1)) = S(S,z,n) & (h . (n + 1)) = o(z,n) from CIRCCMB2:sch 15( A1, A3, A12);



       A14: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) by A1;



       A15: for n be Nat, z be set st z = (h . n) holds (h . (n + 1)) = o(z,n) from CIRCCMB2:sch 3( A14, A13);



       A16: ( dom h) = NAT by PARTFUN1:def 2;



       A17: (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] by A2;



       A18: for n be Nat holds (h . (n + 1)) = F(n,.) by A15;

      consider h1 be ManySortedSet of NAT such that

       A19: (n -BitMajorityOutput (x,y)) = (h1 . n) and

       A20: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] and

       A21: for n be Nat, z be set st z = (h1 . n) holds (h1 . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)) by Def5;



       A22: ( dom h1) = NAT by PARTFUN1:def 2;



       A23: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] by A20;



       A24: for n be Nat holds (h1 . (n + 1)) = F(n,.) by A21;

      h = h1 from NAT_1:sch 15( A16, A17, A18, A22, A23, A24);

      hence thesis by A19;

    end;

    theorem :: FACIRC_2:7



     Th7: for a,b be FinSequence holds ( 0 -BitAdderStr (a,b)) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & ( 0 -BitAdderCirc (a,b)) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) & ( 0 -BitMajorityOutput (a,b)) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )]

    proof

      let a,b be FinSequence;



       A1: ex f,g,h be ManySortedSet of NAT st (( 0 -BitAdderStr (a,b)) = (f . 0 )) & (( 0 -BitAdderCirc (a,b)) = (g . 0 )) & ((f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )))) & ((g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )))) & ((h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )]) & (for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((a . (n + 1)),(b . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((a . (n + 1)),(b . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((a . (n + 1)),(b . (n + 1)),z))) by Def4;

      hence ( 0 -BitAdderStr (a,b)) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

      thus ( 0 -BitAdderCirc (a,b)) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) by A1;

      ( InnerVertices ( 0 -BitAdderStr (a,b))) = { [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )]} by A1, CIRCCOMB: 42;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FACIRC_2:8



     Th8: for a,b be FinSequence, c be set st c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] holds (1 -BitAdderStr (a,b)) = (( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) +* ( BitAdderWithOverflowStr ((a . 1),(b . 1),c))) & (1 -BitAdderCirc (a,b)) = (( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) +* ( BitAdderWithOverflowCirc ((a . 1),(b . 1),c))) & (1 -BitMajorityOutput (a,b)) = ( MajorityOutput ((a . 1),(b . 1),c))

    proof

      let a,b be FinSequence, c be set such that

       A1: c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

      consider f,g,h be ManySortedSet of NAT such that

       A2: (1 -BitAdderStr (a,b)) = (f . 1) and

       A3: (1 -BitAdderCirc (a,b)) = (g . 1) and

       A4: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A5: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A6: (h . 0 ) = c and

       A7: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((a . (n + 1)),(b . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((a . (n + 1)),(b . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((a . (n + 1)),(b . (n + 1)),z)) by A1, Def4;

      (1 -BitMajorityOutput (a,b)) = (h . ( 0 + 1)) by A1, A4, A5, A6, A7, Th6;

      hence thesis by A2, A3, A4, A5, A6, A7;

    end;

    theorem :: FACIRC_2:9

    for a,b,c be set st c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] holds (1 -BitAdderStr ( <*a*>, <*b*>)) = (( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) +* ( BitAdderWithOverflowStr (a,b,c))) & (1 -BitAdderCirc ( <*a*>, <*b*>)) = (( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) +* ( BitAdderWithOverflowCirc (a,b,c))) & (1 -BitMajorityOutput ( <*a*>, <*b*>)) = ( MajorityOutput (a,b,c))

    proof

      let a,b be set;



       A1: ( <*a*> . 1) = a by FINSEQ_1: 40;

      ( <*b*> . 1) = b by FINSEQ_1: 40;

      hence thesis by A1, Th8;

    end;

    theorem :: FACIRC_2:10



     Th10: for n be Nat holds for p,q be FinSeqLen of n holds for p1,p2,q1,q2 be FinSequence holds (n -BitAdderStr ((p ^ p1),(q ^ q1))) = (n -BitAdderStr ((p ^ p2),(q ^ q2))) & (n -BitAdderCirc ((p ^ p1),(q ^ q1))) = (n -BitAdderCirc ((p ^ p2),(q ^ q2))) & (n -BitMajorityOutput ((p ^ p1),(q ^ q1))) = (n -BitMajorityOutput ((p ^ p2),(q ^ q2)))

    proof

      let n be Nat;

      set c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

      let p,q be FinSeqLen of n;

      let p1,p2,q1,q2 be FinSequence;

      deffunc o( set, Nat) = ( MajorityOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1));

      deffunc S( non empty ManySortedSign, set, Nat) = ($1 +* ( BitAdderWithOverflowStr (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2)));

      deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitAdderWithOverflowCirc (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)));

      consider f1,g1,h1 be ManySortedSet of NAT such that

       A1: (n -BitAdderStr ((p ^ p1),(q ^ q1))) = (f1 . n) and

       A2: (n -BitAdderCirc ((p ^ p1),(q ^ q1))) = (g1 . n) and

       A3: (f1 . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A4: (g1 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A5: (h1 . 0 ) = c and

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f1 . n) & A = (g1 . n) & z = (h1 . n) holds (f1 . (n + 1)) = S(S,z,n) & (g1 . (n + 1)) = A(S,A,z,n) & (h1 . (n + 1)) = o(z,n) by Def4;

      consider f2,g2,h2 be ManySortedSet of NAT such that

       A7: (n -BitAdderStr ((p ^ p2),(q ^ q2))) = (f2 . n) and

       A8: (n -BitAdderCirc ((p ^ p2),(q ^ q2))) = (g2 . n) and

       A9: (f2 . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A10: (g2 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A11: (h2 . 0 ) = c and

       A12: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f2 . n) & A = (g2 . n) & z = (h2 . n) holds (f2 . (n + 1)) = (S +* ( BitAdderWithOverflowStr (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z))) & (g2 . (n + 1)) = (A +* ( BitAdderWithOverflowCirc (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z))) & (h2 . (n + 1)) = ( MajorityOutput (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) by Def4;

      defpred L[ Nat] means $1 <= n implies (h1 . $1) = (h2 . $1) & (f1 . $1) = (f2 . $1) & (g1 . $1) = (g2 . $1);



       A13: L[ 0 ] by A3, A4, A5, A9, A10, A11;



       A14: for i be Nat st L[i] holds L[(i + 1)]

      proof

        let i be Nat such that

         A15: i <= n implies (h1 . i) = (h2 . i) & (f1 . i) = (f2 . i) & (g1 . i) = (g2 . i) and

         A16: (i + 1) <= n;



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



         A18: ( len q) = n by CARD_1:def 7;



         A19: ( dom p) = ( Seg n) by A17, FINSEQ_1:def 3;



         A20: ( dom q) = ( Seg n) by A18, FINSEQ_1:def 3;

        ( 0 + 1) <= (i + 1) by XREAL_1: 6;

        then

         A21: (i + 1) in ( Seg n) by A16, FINSEQ_1: 1;

        then

         A22: ((p ^ p1) . (i + 1)) = (p . (i + 1)) by A19, FINSEQ_1:def 7;



         A23: ((p ^ p2) . (i + 1)) = (p . (i + 1)) by A19, A21, FINSEQ_1:def 7;



         A24: ((q ^ q1) . (i + 1)) = (q . (i + 1)) by A20, A21, FINSEQ_1:def 7;



         A25: ((q ^ q2) . (i + 1)) = (q . (i + 1)) by A20, A21, FINSEQ_1:def 7;

        defpred P[ set, set, set, set] means not contradiction;



         A26: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f1 . 0 ) & A = (g1 . 0 ) & x = (h1 . 0 ) & P[S, A, x, 0 ] by A3, A4;



         A27: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f1 . n) & A = (g1 . n) & x = (h1 . n) & P[S, A, x, n] holds P[ S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];



         A28: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set, n be Nat holds A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);

        for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f1 . n) & A = (g1 . n) & P[S, A, (h1 . n), n] from CIRCCMB2:sch 13( A26, A6, A27, A28);

        then

        consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

         A29: S = (f1 . i) and

         A30: A = (g1 . i);



        thus (h1 . (i + 1)) = ( MajorityOutput (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i))) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1: 13

        .= (h2 . (i + 1)) by A12, A15, A16, A29, A30, NAT_1: 13;



        thus (f1 . (i + 1)) = (S +* ( BitAdderWithOverflowStr (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i)))) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1: 13

        .= (f2 . (i + 1)) by A12, A15, A16, A29, A30, NAT_1: 13;



        thus (g1 . (i + 1)) = (A +* ( BitAdderWithOverflowCirc (((p ^ p2) . (i + 1)),((q ^ q2) . (i + 1)),(h2 . i)))) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1: 13

        .= (g2 . (i + 1)) by A12, A15, A16, A29, A30, NAT_1: 13;

      end;



       A31: for i be Nat holds L[i] from NAT_1:sch 2( A13, A14);

      hence (n -BitAdderStr ((p ^ p1),(q ^ q1))) = (n -BitAdderStr ((p ^ p2),(q ^ q2))) & (n -BitAdderCirc ((p ^ p1),(q ^ q1))) = (n -BitAdderCirc ((p ^ p2),(q ^ q2))) by A1, A2, A7, A8;



       A32: (n -BitMajorityOutput ((p ^ p1),(q ^ q1))) = (h1 . n) by A3, A4, A5, A6, Th6;

      (n -BitMajorityOutput ((p ^ p2),(q ^ q2))) = (h2 . n) by A9, A10, A11, A12, Th6;

      hence thesis by A31, A32;

    end;

    theorem :: FACIRC_2:11

    for n be Nat holds for x,y be FinSeqLen of n holds for a,b be set holds ((n + 1) -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>))) = ((n -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr (a,b,(n -BitMajorityOutput (x,y))))) & ((n + 1) -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>))) = ((n -BitAdderCirc (x,y)) +* ( BitAdderWithOverflowCirc (a,b,(n -BitMajorityOutput (x,y))))) & ((n + 1) -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>))) = ( MajorityOutput (a,b,(n -BitMajorityOutput (x,y))))

    proof

      let n be Nat;

      set c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

      let x,y be FinSeqLen of n;

      let a,b be set;

      set p = (x ^ <*a*>), q = (y ^ <*b*>);

      consider f,g,h be ManySortedSet of NAT such that

       A1: (n -BitAdderStr (p,q)) = (f . n) and

       A2: (n -BitAdderCirc (p,q)) = (g . n) and

       A3: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A4: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A5: (h . 0 ) = c and

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((p . (n + 1)),(q . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((p . (n + 1)),(q . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((p . (n + 1)),(q . (n + 1)),z)) by Def4;



       A7: (n -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>))) = (h . n) by A3, A4, A5, A6, Th6;



       A8: ((n + 1) -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>))) = (f . (n + 1)) by A3, A4, A5, A6, Th6;



       A9: ((n + 1) -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>))) = (g . (n + 1)) by A3, A4, A5, A6, Th6;



       A10: ((n + 1) -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>))) = (h . (n + 1)) by A3, A4, A5, A6, Th6;



       A11: ( len x) = n by CARD_1:def 7;



       A12: ( len y) = n by CARD_1:def 7;



       A13: (p . (n + 1)) = a by A11, FINSEQ_1: 42;



       A14: (q . (n + 1)) = b by A12, FINSEQ_1: 42;



       A15: (x ^ <*> ) = x by FINSEQ_1: 34;



       A16: (y ^ <*> ) = y by FINSEQ_1: 34;

      then

       A17: (n -BitAdderStr (p,q)) = (n -BitAdderStr (x,y)) by A15, Th10;



       A18: (n -BitAdderCirc (p,q)) = (n -BitAdderCirc (x,y)) by A15, A16, Th10;

      (n -BitMajorityOutput (p,q)) = (n -BitMajorityOutput (x,y)) by A15, A16, Th10;

      hence thesis by A1, A2, A6, A7, A8, A9, A10, A13, A14, A17, A18;

    end;

    theorem :: FACIRC_2:12



     Th12: for n be Nat holds for x,y be FinSequence holds ((n + 1) -BitAdderStr (x,y)) = ((n -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))) & ((n + 1) -BitAdderCirc (x,y)) = ((n -BitAdderCirc (x,y)) +* ( BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))) & ((n + 1) -BitMajorityOutput (x,y)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))

    proof

      let n be Nat;

      let x,y be FinSequence;

      set c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )];

      consider f,g,h be ManySortedSet of NAT such that

       A1: (n -BitAdderStr (x,y)) = (f . n) and

       A2: (n -BitAdderCirc (x,y)) = (g . n) and

       A3: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A4: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A5: (h . 0 ) = c and

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f . n) & A = (g . n) & z = (h . n) holds (f . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)) by Def4;



       A7: (n -BitMajorityOutput (x,y)) = (h . n) by A3, A4, A5, A6, Th6;



       A8: ((n + 1) -BitAdderStr (x,y)) = (f . (n + 1)) by A3, A4, A5, A6, Th6;



       A9: ((n + 1) -BitAdderCirc (x,y)) = (g . (n + 1)) by A3, A4, A5, A6, Th6;

      ((n + 1) -BitMajorityOutput (x,y)) = (h . (n + 1)) by A3, A4, A5, A6, Th6;

      hence thesis by A1, A2, A6, A7, A8, A9;

    end;

    theorem :: FACIRC_2:13



     Th13: for n,m be Element of NAT st n <= m holds for x,y be FinSequence holds ( InnerVertices (n -BitAdderStr (x,y))) c= ( InnerVertices (m -BitAdderStr (x,y)))

    proof

      let n,m be Element of NAT such that

       A1: n <= m;

      let x,y be FinSequence;

      consider i be Nat such that

       A2: m = (n + i) by A1, NAT_1: 10;

      reconsider i as Element of NAT by ORDINAL1:def 12;



       A3: m = (n + i) by A2;

      defpred L[ Nat] means ( InnerVertices (n -BitAdderStr (x,y))) c= ( InnerVertices ((n + $1) -BitAdderStr (x,y)));



       A4: L[ 0 ];



       A5: for j be Nat st L[j] holds L[(j + 1)]

      proof

        let j be Nat;

        assume

         A6: ( InnerVertices (n -BitAdderStr (x,y))) c= ( InnerVertices ((n + j) -BitAdderStr (x,y)));



         A7: (((n + j) + 1) -BitAdderStr (x,y)) = (((n + j) -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) by Th12;



         A8: ( InnerVertices (((n + j) -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))))) = (( InnerVertices ((n + j) -BitAdderStr (x,y))) \/ ( InnerVertices ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))))) by FACIRC_1: 27;



         A9: ( InnerVertices (n -BitAdderStr (x,y))) c= (( InnerVertices (n -BitAdderStr (x,y))) \/ ( InnerVertices ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))))) by XBOOLE_1: 7;

        (( InnerVertices (n -BitAdderStr (x,y))) \/ ( InnerVertices ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))))) c= (( InnerVertices ((n + j) -BitAdderStr (x,y))) \/ ( InnerVertices ( BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))))) by A6, XBOOLE_1: 9;

        hence thesis by A7, A8, A9, XBOOLE_1: 1;

      end;

      for j be Nat holds L[j] from NAT_1:sch 2( A4, A5);

      hence thesis by A3;

    end;

    theorem :: FACIRC_2:14

    for n be Element of NAT holds for x,y be FinSequence holds ( InnerVertices ((n + 1) -BitAdderStr (x,y))) = (( InnerVertices (n -BitAdderStr (x,y))) \/ ( InnerVertices ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))))

    proof

      let n be Element of NAT ;

      let x,y be FinSequence;

      ((n + 1) -BitAdderStr (x,y)) = ((n -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))) by Th12;

      hence thesis by FACIRC_1: 27;

    end;

    definition

      let k,n be Nat;

      let x,y be FinSequence;

      :: FACIRC_2:def6

      func (k,n) -BitAdderOutput (x,y) -> Element of ( InnerVertices (n -BitAdderStr (x,y))) means

      : Def6: ex i be Element of NAT st k = (i + 1) & it = ( BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))));

      uniqueness ;

      existence

      proof

        consider i be Nat such that

         A3: k = (1 + i) by A1, NAT_1: 10;

        reconsider n9 = n, k9 = k, i as Element of NAT by ORDINAL1:def 12;

        set o = ( BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))));



         A4: ( InnerVertices (k9 -BitAdderStr (x,y))) c= ( InnerVertices (n9 -BitAdderStr (x,y))) by A2, Th13;



         A5: o in ( InnerVertices ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y))))) by A3, FACIRC_1: 90;



         A6: (k -BitAdderStr (x,y)) = ((i -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y))))) by A3, Th12;

        reconsider o as Element of ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) by A5;

        (the carrier of ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) \/ the carrier of (i -BitAdderStr (x,y))) = the carrier of (k -BitAdderStr (x,y)) by A6, CIRCCOMB:def 2;

        then o in the carrier of (k -BitAdderStr (x,y)) by XBOOLE_0:def 3;

        then o in ( InnerVertices (k -BitAdderStr (x,y))) by A5, A6, CIRCCOMB: 15;

        hence thesis by A3, A4;

      end;

    end

    theorem :: FACIRC_2:15

    for n,k be Element of NAT st k < n holds for x,y be FinSequence holds (((k + 1),n) -BitAdderOutput (x,y)) = ( BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y))))

    proof

      let n,k be Element of NAT such that

       A1: k < n;

      let x,y be FinSequence;



       A2: (k + 1) >= 1 by NAT_1: 11;

      (k + 1) <= n by A1, NAT_1: 13;

      then ex i be Element of NAT st ((k + 1) = (i + 1)) & ((((k + 1),n) -BitAdderOutput (x,y)) = ( BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(i -BitMajorityOutput (x,y))))) by A2, Def6;

      hence thesis;

    end;

     Lm1:

    now

      let i be Nat;

      let x be FinSeqLen of (i + 1);



       A1: ( len x) = (i + 1) by CARD_1:def 7;

      consider y be FinSequence, a be object such that

       A2: x = (y ^ <*a*>) by FINSEQ_1: 46;

      ( len <*a*>) = 1 by FINSEQ_1: 40;

      then (i + 1) = (( len y) + 1) by A1, A2, FINSEQ_1: 22;

      then

      reconsider y as FinSeqLen of i by CARD_1:def 7;

      take y, a;

      thus x = (y ^ <*a*>) by A2;

    end;

     Lm2:

    now

      let i be Nat;

      let x be nonpair-yielding FinSeqLen of (i + 1);

      consider y be FinSeqLen of i, a be object such that

       A1: x = (y ^ <*a*>) by Lm1;



       A2: ( dom y) c= ( dom x) by A1, FINSEQ_1: 26;



       A3: y = (x | ( dom y)) by A1, FINSEQ_1: 21;

      y is nonpair-yielding

      proof

        let z be set;

        assume

         A4: z in ( dom y);

        then (y . z) = (x . z) by A3, FUNCT_1: 47;

        hence thesis by A2, A4, FACIRC_1:def 3;

      end;

      then

      reconsider y as nonpair-yielding FinSeqLen of i;



       A5: (i + 1) in ( Seg (i + 1)) by FINSEQ_1: 4;

      ( dom x) = ( Seg ( len x)) by FINSEQ_1:def 3;

      then

       A6: (i + 1) in ( dom x) by A5, CARD_1:def 7;



       A7: (x . (( len y) + 1)) = a by A1, FINSEQ_1: 42;

      ( len y) = i by CARD_1:def 7;

      then

      reconsider a as non pair set by A6, A7, FACIRC_1:def 3;

      take y, a;

      thus x = (y ^ <*a*>) by A1;

    end;

    theorem :: FACIRC_2:16

    for n be Element of NAT holds for x,y be FinSequence holds ( InnerVertices (n -BitAdderStr (x,y))) is Relation

    proof

      let n be Element of NAT ;

      let x,y be FinSequence;

      defpred P[ Nat] means ( InnerVertices ($1 -BitAdderStr (x,y))) is Relation;

      ( 0 -BitAdderStr (x,y)) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) by Th7;

      then

       A1: P[ 0 ] by FACIRC_1: 38;



       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: ( InnerVertices (i -BitAdderStr (x,y))) is Relation;



         A4: ((i + 1) -BitAdderStr (x,y)) = ((i -BitAdderStr (x,y)) +* ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y))))) by Th12;

        ( InnerVertices ( BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y))))) is Relation by FACIRC_1: 88;

        hence thesis by A3, A4, FACIRC_1: 3;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FACIRC_2:17



     Th17: for x,y,c be set holds ( InnerVertices ( MajorityIStr (x,y,c))) = { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]}

    proof

      let x,y,c be set;



       A1: (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' ))) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) by CIRCCOMB: 47;



       A2: ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*y, c*>, '&' )) by CIRCCOMB: 47;

      ( InnerVertices ( MajorityIStr (x,y,c))) = (( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) \/ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by A1, CIRCCOMB: 11

      .= ((( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))) \/ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by A2, CIRCCOMB: 11

      .= (( { [ <*x, y*>, '&' ]} \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))) \/ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by CIRCCOMB: 42

      .= (( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) \/ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by CIRCCOMB: 42

      .= (( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) \/ { [ <*c, x*>, '&' ]}) by CIRCCOMB: 42

      .= ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]} \/ { [ <*c, x*>, '&' ]}) by ENUMSET1: 1

      .= { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: FACIRC_2:18



     Th18: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] holds ( InputVertices ( MajorityIStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be set;

      assume that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ];



       A4: ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*y, c*>, '&' )) by CIRCCOMB: 47;



       A5: y in {1, y} by TARSKI:def 2;



       A6: y in {2, y} by TARSKI:def 2;



       A7: {1, y} in { {1}, {1, y}} by TARSKI:def 2;



       A8: {2, y} in { {2}, {2, y}} by TARSKI:def 2;

       <*y, c*> = ( <*y*> ^ <*c*>) by FINSEQ_1:def 9;

      then

       A9: <*y*> c= <*y, c*> by FINSEQ_6: 10;

       <*y*> = { [1, y]} by FINSEQ_1:def 5;

      then

       A10: [1, y] in <*y*> by TARSKI:def 1;



       A11: <*y, c*> in { <*y, c*>} by TARSKI:def 1;



       A12: { <*y, c*>} in { { <*y, c*>}, { <*y, c*>, '&' }} by TARSKI:def 2;

      then

       A13: y <> [ <*y, c*>, '&' ] by A5, A7, A9, A10, A11, XREGULAR: 9;



       A14: c in {2, c} by TARSKI:def 2;



       A15: {2, c} in { {2}, {2, c}} by TARSKI:def 2;

      ( dom <*y, c*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A16: 2 in ( dom <*y, c*>) by FINSEQ_1: 1;

      ( <*y, c*> . 2) = c by FINSEQ_1: 44;

      then [2, c] in <*y, c*> by A16, FUNCT_1: 1;

      then

       A17: c <> [ <*y, c*>, '&' ] by A11, A12, A14, A15, XREGULAR: 9;

      ( dom <*x, y*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A18: 2 in ( dom <*x, y*>) by FINSEQ_1: 1;

      ( <*x, y*> . 2) = y by FINSEQ_1: 44;

      then

       A19: [2, y] in <*x, y*> by A18, FUNCT_1: 1;



       A20: <*x, y*> in { <*x, y*>} by TARSKI:def 1;

       { <*x, y*>} in { { <*x, y*>}, { <*x, y*>, '&' }} by TARSKI:def 2;

      then y <> [ <*x, y*>, '&' ] by A6, A8, A19, A20, XREGULAR: 9;

      then

       A21: not [ <*x, y*>, '&' ] in {y, c} by A3, TARSKI:def 2;



       A22: x in {1, x} by TARSKI:def 2;



       A23: {1, x} in { {1}, {1, x}} by TARSKI:def 2;

       <*x, y*> = ( <*x*> ^ <*y*>) by FINSEQ_1:def 9;

      then

       A24: <*x*> c= <*x, y*> by FINSEQ_6: 10;

       <*x*> = { [1, x]} by FINSEQ_1:def 5;

      then

       A25: [1, x] in <*x*> by TARSKI:def 1;



       A26: <*x, y*> in { <*x, y*>} by TARSKI:def 1;

       { <*x, y*>} in { { <*x, y*>}, { <*x, y*>, '&' }} by TARSKI:def 2;

      then

       A27: x <> [ <*x, y*>, '&' ] by A22, A23, A24, A25, A26, XREGULAR: 9;



       A28: not c in { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]} by A3, A17, TARSKI:def 2;



       A29: not x in { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]} by A1, A27, TARSKI:def 2;



       A30: x in {2, x} by TARSKI:def 2;



       A31: {2, x} in { {2}, {2, x}} by TARSKI:def 2;

      ( dom <*c, x*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A32: 2 in ( dom <*c, x*>) by FINSEQ_1: 1;

      ( <*c, x*> . 2) = x by FINSEQ_1: 44;

      then

       A33: [2, x] in <*c, x*> by A32, FUNCT_1: 1;



       A34: <*c, x*> in { <*c, x*>} by TARSKI:def 1;

       { <*c, x*>} in { { <*c, x*>}, { <*c, x*>, '&' }} by TARSKI:def 2;

      then

       A35: x <> [ <*c, x*>, '&' ] by A30, A31, A33, A34, XREGULAR: 9;



       A36: c in {1, c} by TARSKI:def 2;



       A37: {1, c} in { {1}, {1, c}} by TARSKI:def 2;

       <*c, x*> = ( <*c*> ^ <*x*>) by FINSEQ_1:def 9;

      then

       A38: <*c*> c= <*c, x*> by FINSEQ_6: 10;

       <*c*> = { [1, c]} by FINSEQ_1:def 5;

      then

       A39: [1, c] in <*c*> by TARSKI:def 1;



       A40: <*c, x*> in { <*c, x*>} by TARSKI:def 1;

       { <*c, x*>} in { { <*c, x*>}, { <*c, x*>, '&' }} by TARSKI:def 2;

      then c <> [ <*c, x*>, '&' ] by A36, A37, A38, A39, A40, XREGULAR: 9;

      then

       A41: not [ <*c, x*>, '&' ] in {x, y, c} by A2, A35, ENUMSET1:def 1;

      ( InputVertices ( MajorityIStr (x,y,c))) = ((( InputVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) \ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))))) \ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))))) \ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ (( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))))) by A4, CIRCCOMB: 11

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))))) \ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ (( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCOMB: 42

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ { [ <*x, y*>, '&' ]})) \ ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' )))) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ (( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCOMB: 42

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ (( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCOMB: 42

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( { [ <*x, y*>, '&' ]} \/ ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' )))))) by CIRCCOMB: 42

      .= ((((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}))) by CIRCCOMB: 42

      .= (((( {x, y} \ { [ <*y, c*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}))) by FACIRC_1: 40

      .= (((( {x, y} \ { [ <*y, c*>, '&' ]}) \/ ( {y, c} \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ (( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) \ ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}))) by FACIRC_1: 40

      .= (((( {x, y} \ { [ <*y, c*>, '&' ]}) \/ ( {y, c} \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ ( {c, x} \ ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}))) by FACIRC_1: 40

      .= (((( {x, y} \ { [ <*y, c*>, '&' ]}) \/ ( {y, c} \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ ( {c, x} \ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]})) by ENUMSET1: 1

      .= ((( {x, y} \/ ( {y, c} \ { [ <*x, y*>, '&' ]})) \ { [ <*c, x*>, '&' ]}) \/ ( {c, x} \ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]})) by A1, A13, Th1

      .= ((( {x, y} \/ {y, c}) \ { [ <*c, x*>, '&' ]}) \/ ( {c, x} \ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]})) by A21, ZFMISC_1: 57

      .= ((( {x, y} \/ {y, c}) \ { [ <*c, x*>, '&' ]}) \/ {c, x}) by A28, A29, ZFMISC_1: 63

      .= (( {x, y, y, c} \ { [ <*c, x*>, '&' ]}) \/ {c, x}) by ENUMSET1: 5

      .= (( {y, y, x, c} \ { [ <*c, x*>, '&' ]}) \/ {c, x}) by ENUMSET1: 67

      .= (( {y, x, c} \ { [ <*c, x*>, '&' ]}) \/ {c, x}) by ENUMSET1: 31

      .= (( {x, y, c} \ { [ <*c, x*>, '&' ]}) \/ {c, x}) by ENUMSET1: 58

      .= ( {x, y, c} \/ {c, x}) by A41, ZFMISC_1: 57

      .= {x, y, c, c, x} by ENUMSET1: 9

      .= ( {x, y, c, c} \/ {x}) by ENUMSET1: 10

      .= ( {c, c, x, y} \/ {x}) by ENUMSET1: 73

      .= ( {c, x, y} \/ {x}) by ENUMSET1: 31

      .= {c, x, y, x} by ENUMSET1: 6

      .= {x, x, y, c} by ENUMSET1: 70

      .= {x, y, c} by ENUMSET1: 31;

      hence thesis;

    end;

    theorem :: FACIRC_2:19



     Th19: for x,y,c be set holds ( InnerVertices ( MajorityStr (x,y,c))) = ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))})

    proof

      let x,y,c be set;

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set Cxy = ( 1GateCircStr ( <*x, y*>, '&' )), Cyc = ( 1GateCircStr ( <*y, c*>, '&' )), Ccx = ( 1GateCircStr ( <*c, x*>, '&' )), Cxyc = ( 1GateCircStr ( <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ));



       A1: Cxy tolerates ((Cyc +* Ccx) +* Cxyc) by CIRCCOMB: 47;



       A2: Cyc tolerates (Ccx +* Cxyc) by CIRCCOMB: 47;



       A3: Ccx tolerates Cxyc by CIRCCOMB: 47;



       A4: ( InnerVertices (Cyc +* (Ccx +* Cxyc))) = (( InnerVertices Cyc) \/ ( InnerVertices (Ccx +* Cxyc))) by A2, CIRCCOMB: 11;



       A5: ( InnerVertices (Ccx +* Cxyc)) = (( InnerVertices Ccx) \/ ( InnerVertices Cxyc)) by A3, CIRCCOMB: 11;



      thus ( InnerVertices ( MajorityStr (x,y,c))) = ( InnerVertices ((Cxy +* (Cyc +* Ccx)) +* Cxyc)) by CIRCCOMB: 6

      .= ( InnerVertices (Cxy +* ((Cyc +* Ccx) +* Cxyc))) by CIRCCOMB: 6

      .= (( InnerVertices Cxy) \/ ( InnerVertices ((Cyc +* Ccx) +* Cxyc))) by A1, CIRCCOMB: 11

      .= (( InnerVertices Cxy) \/ ( InnerVertices (Cyc +* (Ccx +* Cxyc)))) by CIRCCOMB: 6

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyc)) \/ (( InnerVertices Ccx) \/ ( InnerVertices Cxyc))) by A4, A5, XBOOLE_1: 4

      .= (((( InnerVertices Cxy) \/ ( InnerVertices Cyc)) \/ ( InnerVertices Ccx)) \/ ( InnerVertices Cxyc)) by XBOOLE_1: 4

      .= ((( {xy} \/ ( InnerVertices Cyc)) \/ ( InnerVertices Ccx)) \/ ( InnerVertices Cxyc)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yc}) \/ ( InnerVertices Ccx)) \/ ( InnerVertices Cxyc)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yc}) \/ {cx}) \/ ( InnerVertices Cxyc)) by CIRCCOMB: 42

      .= (( {xy, yc} \/ {cx}) \/ ( InnerVertices Cxyc)) by ENUMSET1: 1

      .= ( {xy, yc, cx} \/ ( InnerVertices Cxyc)) by ENUMSET1: 3

      .= ( {xy, yc, cx} \/ {( MajorityOutput (x,y,c))}) by CIRCCOMB: 42;

    end;

    theorem :: FACIRC_2:20



     Th20: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] holds ( InputVertices ( MajorityStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be set;

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set S = ( 1GateCircStr ( <*xy, yc, cx*>, or3 ));



       A1: ( InnerVertices S) = { [ <*xy, yc, cx*>, or3 ]} by CIRCCOMB: 42;



       A2: ( InputVertices S) = ( rng <*xy, yc, cx*>) by CIRCCOMB: 42

      .= {xy, yc, cx} by FINSEQ_2: 128;

      set MI = ( MajorityIStr (x,y,c));

      assume that

       A3: x <> yc and

       A4: y <> cx and

       A5: c <> xy;

      ( rng <*c, x*>) = {c, x} by FINSEQ_2: 127;

      then

       A6: x in ( rng <*c, x*>) by TARSKI:def 2;

      ( len <*xy, yc, cx*>) = 3 by FINSEQ_1: 45;

      then

       A7: ( Seg 3) = ( dom <*xy, yc, cx*>) by FINSEQ_1:def 3;

      then

       A8: 3 in ( dom <*xy, yc, cx*>) by FINSEQ_1: 1;

      ( <*xy, yc, cx*> . 3) = cx by FINSEQ_1: 45;

      then [3, cx] in <*xy, yc, cx*> by A8, FUNCT_1: 1;

      then cx in ( rng <*xy, yc, cx*>) by XTUPLE_0:def 13;

      then

       A9: ( the_rank_of cx) in ( the_rank_of [ <*xy, yc, cx*>, or3 ]) by CLASSES1: 82;

      ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      then

       A10: y in ( rng <*x, y*>) by TARSKI:def 2;



       A11: 1 in ( dom <*xy, yc, cx*>) by A7, FINSEQ_1: 1;

      ( <*xy, yc, cx*> . 1) = xy by FINSEQ_1: 45;

      then [1, xy] in <*xy, yc, cx*> by A11, FUNCT_1: 1;

      then xy in ( rng <*xy, yc, cx*>) by XTUPLE_0:def 13;

      then

       A12: ( the_rank_of xy) in ( the_rank_of [ <*xy, yc, cx*>, or3 ]) by CLASSES1: 82;

      ( rng <*y, c*>) = {y, c} by FINSEQ_2: 127;

      then

       A13: c in ( rng <*y, c*>) by TARSKI:def 2;



       A14: 2 in ( dom <*xy, yc, cx*>) by A7, FINSEQ_1: 1;

      ( <*xy, yc, cx*> . 2) = yc by FINSEQ_1: 45;

      then [2, yc] in <*xy, yc, cx*> by A14, FUNCT_1: 1;

      then yc in ( rng <*xy, yc, cx*>) by XTUPLE_0:def 13;

      then

       A15: ( the_rank_of yc) in ( the_rank_of [ <*xy, yc, cx*>, or3 ]) by CLASSES1: 82;



       A16: ( {xy, yc, cx} \ {xy, yc, cx}) = {} by XBOOLE_1: 37;



       A17: ( {x, y, c} \ { [ <*xy, yc, cx*>, or3 ]}) = {x, y, c}

      proof

        thus ( {x, y, c} \ { [ <*xy, yc, cx*>, or3 ]}) c= {x, y, c};

        let a be object;

        assume

         A18: a in {x, y, c};

        then a = x or a = y or a = c by ENUMSET1:def 1;

        then a <> [ <*xy, yc, cx*>, or3 ] by A6, A9, A10, A12, A13, A15, CLASSES1: 82;

        then not a in { [ <*xy, yc, cx*>, or3 ]} by TARSKI:def 1;

        hence thesis by A18, XBOOLE_0:def 5;

      end;



      thus ( InputVertices ( MajorityStr (x,y,c))) = ((( InputVertices MI) \ ( InnerVertices S)) \/ (( InputVertices S) \ ( InnerVertices MI))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ( {x, y, c} \/ ( {xy, yc, cx} \ ( InnerVertices MI))) by A1, A2, A3, A4, A5, A17, Th18

      .= ( {x, y, c} \/ {} ) by A16, Th17

      .= {x, y, c};

    end;

    theorem :: FACIRC_2:21



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

    proof

      let S1,S2 be non empty ManySortedSign such that

       A1: S1 tolerates S2 and

       A2: ( InputVertices S1) = ( InputVertices S2);



       A3: ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;



       A4: ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;



      thus ( InputVertices (S1 +* S2)) = ((( InputVertices S1) \ ( InnerVertices S2)) \/ (( InputVertices S2) \ ( InnerVertices S1))) by A1, CIRCCMB2: 5

      .= (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by A2, A4, XBOOLE_1: 83

      .= (( InputVertices S1) \/ ( InputVertices S2)) by A2, A3, XBOOLE_1: 83

      .= ( InputVertices S1) by A2;

    end;

    theorem :: FACIRC_2:22



     Th22: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] & c <> [ <*x, y*>, 'xor' ] holds ( InputVertices ( BitAdderWithOverflowStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be set such that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ] and

       A4: c <> [ <*x, y*>, 'xor' ];



       A5: ( InputVertices ( 2GatesCircStr (x,y,c, 'xor' ))) = {x, y, c} by A4, FACIRC_1: 57;

      ( InputVertices ( MajorityStr (x,y,c))) = {x, y, c} by A1, A2, A3, Th20;

      hence thesis by A5, Th21, CIRCCOMB: 47;

    end;

    theorem :: FACIRC_2:23



     Th23: for x,y,c be set holds ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) = (( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]}) \/ {( MajorityOutput (x,y,c))})

    proof

      let x,y,c be set;

      ( 2GatesCircStr (x,y,c, 'xor' )) tolerates ( MajorityStr (x,y,c)) by CIRCCOMB: 47;



      then ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) = (( InnerVertices ( 2GatesCircStr (x,y,c, 'xor' ))) \/ ( InnerVertices ( MajorityStr (x,y,c)))) by CIRCCOMB: 11

      .= ( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ ( InnerVertices ( MajorityStr (x,y,c)))) by FACIRC_1: 56

      .= ( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))})) by Th19

      .= (( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]}) \/ {( MajorityOutput (x,y,c))}) by XBOOLE_1: 4;

      hence thesis;

    end;

    registration

      cluster empty -> non pair for set;

      coherence ;

    end

    registration

      cluster empty -> nonpair-yielding for Function;

      coherence

      proof

        let F be Function such that

         A1: F is empty;

        let x be set;

        assume x in ( dom F);

        thus thesis by A1;

      end;

      let f be nonpair-yielding Function;

      let x be set;

      cluster (f . x) -> non pair;

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

          hence thesis by FACIRC_1:def 3;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let n be Nat;

      let x,y be FinSequence;

      cluster (n -BitMajorityOutput (x,y)) -> pair;

      coherence

      proof



         A1: ex h be ManySortedSet of NAT st (( 0 -BitMajorityOutput (x,y)) = (h . 0 )) & ((h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )]) & (for n be Nat, z be set st z = (h . n) holds (h . (n + 1)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),z))) by Def5;

        defpred P[ Nat] means ($1 -BitMajorityOutput (x,y)) is pair;



         A2: P[ 0 ] by A1;



         A3: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          ((n + 1) -BitMajorityOutput (x,y)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) by Th12

          .= [ <* [ <*(x . (n + 1)), (y . (n + 1))*>, '&' ], [ <*(y . (n + 1)), (n -BitMajorityOutput (x,y))*>, '&' ], [ <*(n -BitMajorityOutput (x,y)), (x . (n + 1))*>, '&' ]*>, or3 ];

          hence thesis;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

        hence thesis;

      end;

    end

    theorem :: FACIRC_2:24



     Th24: for x,y be FinSequence, n be Nat holds ((n -BitMajorityOutput (x,y)) `1 ) = <*> & ((n -BitMajorityOutput (x,y)) `2 ) = (( 0 -tuples_on BOOLEAN ) --> FALSE ) & ( proj1 ((n -BitMajorityOutput (x,y)) `2 )) = ( 0 -tuples_on BOOLEAN ) or ( card ((n -BitMajorityOutput (x,y)) `1 )) = 3 & ((n -BitMajorityOutput (x,y)) `2 ) = or3 & ( proj1 ((n -BitMajorityOutput (x,y)) `2 )) = (3 -tuples_on BOOLEAN )

    proof

      let x,y be FinSequence;

      defpred P[ Nat] means (($1 -BitMajorityOutput (x,y)) `1 ) = <*> & (($1 -BitMajorityOutput (x,y)) `2 ) = (( 0 -tuples_on BOOLEAN ) --> FALSE ) & ( proj1 (($1 -BitMajorityOutput (x,y)) `2 )) = ( 0 -tuples_on BOOLEAN ) or ( card (($1 -BitMajorityOutput (x,y)) `1 )) = 3 & (($1 -BitMajorityOutput (x,y)) `2 ) = or3 & ( proj1 (($1 -BitMajorityOutput (x,y)) `2 )) = (3 -tuples_on BOOLEAN );



       A1: ( dom (( 0 -tuples_on BOOLEAN ) --> FALSE )) = ( 0 -tuples_on BOOLEAN ) by FUNCOP_1: 13;

      ( 0 -BitMajorityOutput (x,y)) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] by Th7;

      then

       A2: P[ 0 ] by A1;

       A3:

      now

        let n be Nat;

        assume P[n];

        set c = (n -BitMajorityOutput (x,y));



         A4: ((n + 1) -BitMajorityOutput (x,y)) = ( MajorityOutput ((x . (n + 1)),(y . (n + 1)),c)) by Th12

        .= [ <* [ <*(x . (n + 1)), (y . (n + 1))*>, '&' ], [ <*(y . (n + 1)), c*>, '&' ], [ <*c, (x . (n + 1))*>, '&' ]*>, or3 ];



         A5: ( dom or3 ) = (3 -tuples_on BOOLEAN ) by FUNCT_2:def 1;

        thus P[(n + 1)] by A4, A5, FINSEQ_1: 45;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

    end;

    theorem :: FACIRC_2:25



     Th25: for n be Nat, x,y be FinSequence, p be set holds (n -BitMajorityOutput (x,y)) <> [p, '&' ] & (n -BitMajorityOutput (x,y)) <> [p, 'xor' ]

    proof

      let n be Nat, x,y be FinSequence, p be set;



       A1: ( dom '&' ) = (2 -tuples_on BOOLEAN ) by FUNCT_2:def 1;



       A2: ( dom 'xor' ) = (2 -tuples_on BOOLEAN ) by FUNCT_2:def 1;



       A3: ( proj1 ( [p, '&' ] `2 )) = (2 -tuples_on BOOLEAN ) by A1;



       A4: ( proj1 ( [p, 'xor' ] `2 )) = (2 -tuples_on BOOLEAN ) by A2;

      ( proj1 ((n -BitMajorityOutput (x,y)) `2 )) = ( 0 -tuples_on BOOLEAN ) or ( proj1 ((n -BitMajorityOutput (x,y)) `2 )) = (3 -tuples_on BOOLEAN ) by Th24;

      hence thesis by A3, A4, FINSEQ_2: 110;

    end;

    theorem :: FACIRC_2:26



     Th26: for f,g be nonpair-yielding FinSequence holds for n be Nat holds ( InputVertices ((n + 1) -BitAdderStr (f,g))) = (( InputVertices (n -BitAdderStr (f,g))) \/ (( InputVertices ( BitAdderWithOverflowStr ((f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput (f,g))))) \ {(n -BitMajorityOutput (f,g))})) & ( InnerVertices (n -BitAdderStr (f,g))) is Relation & ( InputVertices (n -BitAdderStr (f,g))) is without_pairs

    proof

      let f,g be nonpair-yielding FinSequence;

      deffunc Sn( Nat) = ($1 -BitAdderStr (f,g));

      deffunc S( set, Nat) = ( BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1));

      deffunc H( Nat) = ($1 -BitMajorityOutput (f,g));

      consider h be ManySortedSet of NAT such that

       A1: for n be Element of NAT holds (h . n) = H(n) from PBOOLE:sch 5;



       A2: for n be Nat holds (h . n) = H(n)

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      deffunc h( Nat) = (h . $1);

      deffunc o( set, Nat) = ( MajorityOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1));

      set k = (( 0 -tuples_on BOOLEAN ) --> FALSE );



       A3: ( 0 -BitAdderStr (f,g)) = ( 1GateCircStr ( <*> ,k)) by Th7;

      then

       A4: ( InnerVertices Sn(0)) is Relation by FACIRC_1: 38;



       A5: ( InputVertices Sn(0)) is without_pairs by A3, FACIRC_1: 39;

       h(0) = ( 0 -BitMajorityOutput (f,g)) by A2;

      then

       A6: (h . 0 ) in ( InnerVertices Sn(0));



       A7: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation by FACIRC_1: 88;

       A8:

      now

        let n be Nat, x be set such that

         A9: x = h(n);



         A10: h(n) = (n -BitMajorityOutput (f,g)) by A2;

        then

         A11: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, '&' ] by A9, Th25;

        x <> [ <*(f . (n + 1)), (g . (n + 1))*>, 'xor' ] by A9, A10, Th25;

        hence ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A11, Th22;

      end;



       A12: for n be Nat, x be set st x = (h . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs

      proof

        let n be Nat, x be set;

        assume x = h(n);

        then

         A13: ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A8;

        thus (( InputVertices S(x,n)) \ {x}) is without_pairs

        proof

          let a be pair object;

          assume

           A14: a in (( InputVertices S(x,n)) \ {x});

          then a in ( InputVertices S(x,n)) by XBOOLE_0:def 5;

          then

           A15: a = (f . (n + 1)) or a = (g . (n + 1)) or a = x by A13, ENUMSET1:def 1;

           not a in {x} by A14, XBOOLE_0:def 5;

          hence contradiction by A15, TARSKI:def 1;

        end;

      end;

       A16:

      now

        let n be Nat, S be non empty ManySortedSign, x be set;

        assume that

         A17: S = Sn(n) and

         A18: x = (h . n);



         A19: x = (n -BitMajorityOutput (f,g)) by A2, A18;



         A20: h(+) = ((n + 1) -BitMajorityOutput (f,g)) by A2;

        thus Sn(+) = (S +* S(x,n)) by A17, A19, Th12;

        thus (h . (n + 1)) = o(x,n) by A19, A20, Th12;

        ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A8, A18;

        hence x in ( InputVertices S(x,n)) by ENUMSET1:def 1;



         A21: ( InnerVertices S(x,n)) = (( { [ <*(f . (n + 1)), (g . (n + 1))*>, 'xor' ], ( 2GatesCircOutput ((f . (n + 1)),(g . (n + 1)),x, 'xor' ))} \/ { [ <*(f . (n + 1)), (g . (n + 1))*>, '&' ], [ <*(g . (n + 1)), x*>, '&' ], [ <*x, (f . (n + 1))*>, '&' ]}) \/ {( MajorityOutput ((f . (n + 1)),(g . (n + 1)),x))}) by Th23;

         o(x,n) in { o(x,n)} by TARSKI:def 1;

        hence o(x,n) in ( InnerVertices S(x,n)) by A21, XBOOLE_0:def 3;

      end;



       A22: for n be Nat holds ( InputVertices Sn(+)) = (( InputVertices Sn(n)) \/ (( InputVertices S(.,n)) \ {(h . n)})) & ( InnerVertices Sn(n)) is Relation & ( InputVertices Sn(n)) is without_pairs from CIRCCMB2:sch 11( A4, A5, A6, A7, A12, A16);

      let n be Nat;

      (h . n) = (n -BitMajorityOutput (f,g)) by A2;

      hence thesis by A22;

    end;

    theorem :: FACIRC_2:27

    for n be Nat holds for x,y be nonpair-yielding FinSeqLen of n holds ( InputVertices (n -BitAdderStr (x,y))) = (( rng x) \/ ( rng y))

    proof

      defpred P[ Nat] means for x,y be nonpair-yielding FinSeqLen of $1 holds ( InputVertices ($1 -BitAdderStr (x,y))) = (( rng x) \/ ( rng y));



       A1: P[ 0 ]

      proof

        let x,y be nonpair-yielding FinSeqLen of 0 ;

        set f = (( 0 -tuples_on BOOLEAN ) --> FALSE );

        ( 0 -BitAdderStr (x,y)) = ( 1GateCircStr ( <*> ,f)) by Th7;

        hence thesis by CIRCCOMB: 42;

      end;



       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A3: P[i];

        let x,y be nonpair-yielding FinSeqLen of (i + 1);

        consider x9 be nonpair-yielding FinSeqLen of i, z1 be non pair set such that

         A4: x = (x9 ^ <*z1*>) by Lm2;

        consider y9 be nonpair-yielding FinSeqLen of i, z2 be non pair set such that

         A5: y = (y9 ^ <*z2*>) by Lm2;

        set S = ((i + 1) -BitAdderStr (x,y));



         A6: 1 in ( Seg 1) by FINSEQ_1: 1;



         A7: ( dom <*z1*>) = ( Seg 1) by FINSEQ_1:def 8;



         A8: ( <*z1*> . 1) = z1 by FINSEQ_1:def 8;

        ( len x9) = i by CARD_1:def 7;

        then

         A9: (x . (i + 1)) = z1 by A4, A6, A7, A8, FINSEQ_1:def 7;



         A10: ( dom <*z2*>) = ( Seg 1) by FINSEQ_1:def 8;



         A11: ( <*z2*> . 1) = z2 by FINSEQ_1:def 8;

        ( len y9) = i by CARD_1:def 7;

        then

         A12: (y . (i + 1)) = z2 by A5, A6, A10, A11, FINSEQ_1:def 7;



         A13: {z1, z2, (i -BitMajorityOutput (x,y))} = {(i -BitMajorityOutput (x,y)), z1, z2} by ENUMSET1: 59;



         A14: ( rng x) = (( rng x9) \/ ( rng <*z1*>)) by A4, FINSEQ_1: 31

        .= (( rng x9) \/ {z1}) by FINSEQ_1: 38;



         A15: ( rng y) = (( rng y9) \/ ( rng <*z2*>)) by A5, FINSEQ_1: 31

        .= (( rng y9) \/ {z2}) by FINSEQ_1: 38;



         A16: (i -BitMajorityOutput (x,y)) <> [ <*z1, z2*>, '&' ] by Th25;



         A17: (i -BitMajorityOutput (x,y)) <> [ <*z1, z2*>, 'xor' ] by Th25;



         A18: x9 = (x9 ^ {} ) by FINSEQ_1: 34;

        y9 = (y9 ^ {} ) by FINSEQ_1: 34;

        then (i -BitAdderStr (x,y)) = (i -BitAdderStr (x9,y9)) by A4, A5, A18, Th10;



        hence ( InputVertices S) = (( InputVertices (i -BitAdderStr (x9,y9))) \/ (( InputVertices ( BitAdderWithOverflowStr (z1,z2,(i -BitMajorityOutput (x,y))))) \ {(i -BitMajorityOutput (x,y))})) by A9, A12, Th26

        .= ((( rng x9) \/ ( rng y9)) \/ (( InputVertices ( BitAdderWithOverflowStr (z1,z2,(i -BitMajorityOutput (x,y))))) \ {(i -BitMajorityOutput (x,y))})) by A3

        .= ((( rng x9) \/ ( rng y9)) \/ ( {z1, z2, (i -BitMajorityOutput (x,y))} \ {(i -BitMajorityOutput (x,y))})) by A16, A17, Th22

        .= ((( rng x9) \/ ( rng y9)) \/ {z1, z2}) by A13, ENUMSET1: 86

        .= ((( rng x9) \/ ( rng y9)) \/ ( {z1} \/ {z2})) by ENUMSET1: 1

        .= (((( rng x9) \/ ( rng y9)) \/ {z1}) \/ {z2}) by XBOOLE_1: 4

        .= (((( rng x9) \/ {z1}) \/ ( rng y9)) \/ {z2}) by XBOOLE_1: 4

        .= (( rng x) \/ ( rng y)) by A14, A15, XBOOLE_1: 4;

      end;

      thus for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

    end;



     Lm3: for x,y,c be set holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following s) . [ <*x, y*>, '&' ]) = (a1 '&' a2) & (( Following s) . [ <*y, c*>, '&' ]) = (a2 '&' a3) & (( Following s) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be set;

      let s be State of ( MajorityCirc (x,y,c));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . c);

      set S = ( MajorityStr (x,y,c));



       A4: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;



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



       A6: x in the carrier of S by FACIRC_1: 72;



       A7: y in the carrier of S by FACIRC_1: 72;



       A8: c in the carrier of S by FACIRC_1: 72;

       [ <*x, y*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by FACIRC_1: 73;



      hence (( Following s) . [ <*x, y*>, '&' ]) = ( '&' . (s * <*x, y*>)) by A4, FACIRC_1: 35

      .= ( '&' . <*a1, a2*>) by A1, A2, A5, A6, A7, FINSEQ_2: 125

      .= (a1 '&' a2) by FACIRC_1:def 6;

       [ <*y, c*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by FACIRC_1: 73;



      hence (( Following s) . [ <*y, c*>, '&' ]) = ( '&' . (s * <*y, c*>)) by A4, FACIRC_1: 35

      .= ( '&' . <*a2, a3*>) by A2, A3, A5, A7, A8, FINSEQ_2: 125

      .= (a2 '&' a3) by FACIRC_1:def 6;

       [ <*c, x*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by FACIRC_1: 73;



      hence (( Following s) . [ <*c, x*>, '&' ]) = ( '&' . (s * <*c, x*>)) by A4, FACIRC_1: 35

      .= ( '&' . <*a3, a1*>) by A1, A3, A5, A6, A8, FINSEQ_2: 125

      .= (a3 '&' a1) by FACIRC_1:def 6;

    end;

    theorem :: FACIRC_2:28



     Th28: for x,y,c be set holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, '&' ]) & a2 = (s . [ <*y, c*>, '&' ]) & a3 = (s . [ <*c, x*>, '&' ]) holds (( Following s) . ( MajorityOutput (x,y,c))) = ((a1 'or' a2) 'or' a3)

    proof

      let x,y,c be set;

      let s be State of ( MajorityCirc (x,y,c));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . [ <*x, y*>, '&' ]) and

       A2: a2 = (s . [ <*y, c*>, '&' ]) and

       A3: a3 = (s . [ <*c, x*>, '&' ]);

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set S = ( MajorityStr (x,y,c));



       A4: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;



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

      reconsider xy, yc, cx as Element of ( InnerVertices S) by FACIRC_1: 73;



      thus (( Following s) . ( MajorityOutput (x,y,c))) = ( or3 . (s * <*xy, yc, cx*>)) by A4, FACIRC_1: 35

      .= ( or3 . <*a1, a2, a3*>) by A1, A2, A3, A5, FINSEQ_2: 126

      .= ((a1 'or' a2) 'or' a3) by FACIRC_1:def 7;

    end;



     Lm4: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . [ <*x, y*>, '&' ]) = (a1 '&' a2) & (( Following (s,2)) . [ <*y, c*>, '&' ]) = (a2 '&' a3) & (( Following (s,2)) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be set such that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ];

      let s be State of ( MajorityCirc (x,y,c));

      let a1,a2,a3 be Element of BOOLEAN such that

       A4: a1 = (s . x) and

       A5: a2 = (s . y) and

       A6: a3 = (s . c);

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set S = ( MajorityStr (x,y,c));

      reconsider x9 = x, y9 = y, c9 = c as Vertex of S by FACIRC_1: 72;



       A7: ( InputVertices S) = {x, y, c} by A1, A2, A3, Th20;

      then

       A8: x in ( InputVertices S) by ENUMSET1:def 1;



       A9: y in ( InputVertices S) by A7, ENUMSET1:def 1;



       A10: c in ( InputVertices S) by A7, ENUMSET1:def 1;



       A11: (( Following s) . x9) = (s . x) by A8, CIRCUIT2:def 5;



       A12: (( Following s) . y9) = (s . y) by A9, CIRCUIT2:def 5;



       A13: (( Following s) . c9) = (s . c) by A10, CIRCUIT2:def 5;



       A14: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;



       A15: (( Following s) . xy) = (a1 '&' a2) by A4, A5, A6, Lm3;



       A16: (( Following s) . yc) = (a2 '&' a3) by A4, A5, A6, Lm3;

      (( Following s) . cx) = (a3 '&' a1) by A4, A5, A6, Lm3;

      hence (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A14, A15, A16, Th28;

      thus thesis by A4, A5, A6, A11, A12, A13, A14, Lm3;

    end;

    theorem :: FACIRC_2:29



     Th29: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] holds for s be State of ( MajorityCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be set;

      set S = ( MajorityStr (x,y,c));

      assume that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ];

      let s be State of ( MajorityCirc (x,y,c));



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



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

      reconsider xx = x, yy = y, cc = c as Vertex of S by FACIRC_1: 72;

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . cc);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);



       A6: a1 = (s . x);



       A7: a2 = (s . y);



       A8: a3 = (s . c);



       A9: (ffs . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A1, A2, A3, Lm4;



       A10: (ffs . [ <*x, y*>, '&' ]) = (a1 '&' a2) by A1, A2, A3, A8, Lm4;



       A11: (ffs . [ <*y, c*>, '&' ]) = (a2 '&' a3) by A1, A2, A3, A6, Lm4;



       A12: (ffs . [ <*c, x*>, '&' ]) = (a3 '&' a1) by A1, A2, A3, A7, Lm4;



       A13: ffs = ( Following ( Following s)) by FACIRC_1: 15;



       A14: ( InputVertices S) = {x, y, c} by A1, A2, A3, Th20;

      then

       A15: x in ( InputVertices S) by ENUMSET1:def 1;



       A16: y in ( InputVertices S) by A14, ENUMSET1:def 1;



       A17: c in ( InputVertices S) by A14, ENUMSET1:def 1;



       A18: (( Following s) . x) = a1 by A15, CIRCUIT2:def 5;



       A19: (( Following s) . y) = a2 by A16, CIRCUIT2:def 5;



       A20: (( Following s) . c) = a3 by A17, CIRCUIT2:def 5;



       A21: (ffs . x) = a1 by A13, A15, A18, CIRCUIT2:def 5;



       A22: (ffs . y) = a2 by A13, A16, A19, CIRCUIT2:def 5;



       A23: (ffs . c) = a3 by A13, A17, A20, CIRCUIT2:def 5;

      now

        let a be object;

        assume

         A24: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;



         A25: v in (( InputVertices S) \/ ( InnerVertices S)) by A24, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A25, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))}) by Th19;

            then v in { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} or v in {( MajorityOutput (x,y,c))} by XBOOLE_0:def 3;

            then v = [ <*x, y*>, '&' ] or v = [ <*y, c*>, '&' ] or v = [ <*c, x*>, '&' ] or v = ( MajorityOutput (x,y,c)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A9, A10, A11, A12, A21, A22, A23, Lm3, Th28;

          end;

        end;

      end;

      hence ffs = fffs by A4, A5, FUNCT_1: 2;

    end;

    theorem :: FACIRC_2:30

    for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] & c <> [ <*x, y*>, 'xor' ] holds for s be State of ( BitAdderWithOverflowCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( BitAdderOutput (x,y,c))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1))

    proof

      let x,y,c be set such that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ] and

       A4: c <> [ <*x, y*>, 'xor' ];

      set f = 'xor' ;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      set A = ( BitAdderWithOverflowCirc (x,y,c));

      set A1 = ( BitAdderCirc (x,y,c)), A2 = ( MajorityCirc (x,y,c));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A5: a1 = (s . x) and

       A6: a2 = (s . y) and

       A7: a3 = (s . c);



       A8: x in the carrier of S1 by FACIRC_1: 60;



       A9: y in the carrier of S1 by FACIRC_1: 60;



       A10: c in the carrier of S1 by FACIRC_1: 60;



       A11: x in the carrier of S2 by FACIRC_1: 72;



       A12: y in the carrier of S2 by FACIRC_1: 72;



       A13: c in the carrier of S2 by FACIRC_1: 72;

      reconsider s1 = (s | the carrier of S1) as State of A1 by FACIRC_1: 26;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      reconsider t = s as State of (A1 +* A2);

      ( InputVertices S1) = {x, y, c} by A4, FACIRC_1: 57;

      then

       A14: ( InputVertices S1) = ( InputVertices S2) by A1, A2, A3, Th20;



       A15: ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;



       A16: ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;



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

      then

       A18: a1 = (s1 . x) by A5, A8, FUNCT_1: 47;



       A19: a2 = (s1 . y) by A6, A9, A17, FUNCT_1: 47;



       A20: a3 = (s1 . c) by A7, A10, A17, FUNCT_1: 47;

      (( Following (t,2)) . ( 2GatesCircOutput (x,y,c,f))) = (( Following (s1,2)) . ( 2GatesCircOutput (x,y,c,f))) by A14, A16, FACIRC_1: 32;

      hence (( Following (s,2)) . ( BitAdderOutput (x,y,c))) = ((a1 'xor' a2) 'xor' a3) by A4, A18, A19, A20, FACIRC_1: 64;



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

      then

       A22: a1 = (s2 . x) by A5, A11, FUNCT_1: 47;



       A23: a2 = (s2 . y) by A6, A12, A21, FUNCT_1: 47;



       A24: a3 = (s2 . c) by A7, A13, A21, FUNCT_1: 47;

      (( Following (t,2)) . ( MajorityOutput (x,y,c))) = (( Following (s2,2)) . ( MajorityOutput (x,y,c))) by A14, A15, FACIRC_1: 33;

      hence thesis by A1, A2, A3, A22, A23, A24, Lm4;

    end;

    theorem :: FACIRC_2:31



     Th31: for x,y,c be set st x <> [ <*y, c*>, '&' ] & y <> [ <*c, x*>, '&' ] & c <> [ <*x, y*>, '&' ] & c <> [ <*x, y*>, 'xor' ] holds for s be State of ( BitAdderWithOverflowCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be set such that

       A1: x <> [ <*y, c*>, '&' ] and

       A2: y <> [ <*c, x*>, '&' ] and

       A3: c <> [ <*x, y*>, '&' ] and

       A4: c <> [ <*x, y*>, 'xor' ];

      set S = ( BitAdderWithOverflowStr (x,y,c));

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      set A = ( BitAdderWithOverflowCirc (x,y,c));

      set A1 = ( BitAdderCirc (x,y,c)), A2 = ( MajorityCirc (x,y,c));

      let s be State of A;

      reconsider s1 = (s | the carrier of S1) as State of A1 by FACIRC_1: 26;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      reconsider t = s as State of (A1 +* A2);

      ( InputVertices S1) = {x, y, c} by A4, FACIRC_1: 57;

      then

       A5: ( InputVertices S1) = ( InputVertices S2) by A1, A2, A3, Th20;



       A6: ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;



       A7: ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A8: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) by A5, FACIRC_1: 30;



       A9: ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by A5, A7, FACIRC_1: 30;



       A10: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) by A5, A6, FACIRC_1: 31;



       A11: ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A5, A6, FACIRC_1: 31;

      ( Following (s1,2)) is stable by A4, FACIRC_1: 63;



      then

       A12: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      ( Following (s2,2)) is stable by A1, A2, A3, Th29;



      then

       A13: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;



       A14: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;



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



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



       A17: ( dom ( Following (s1,2))) = the carrier of S1 by CIRCUIT1: 3;



       A18: ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;



       A19: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 by A19, XBOOLE_0:def 3;

        then (( Following (s,2)) . a) = (( Following (s1,2)) . a) & (( Following (s,3)) . a) = (( Following (s1,3)) . a) or (( Following (s,2)) . a) = (( Following (s2,2)) . a) & (( Following (s,3)) . a) = (( Following (s2,3)) . a) by A8, A9, A10, A11, A12, A13, A17, A18, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A12, A13, FACIRC_1: 12;

      end;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A14, A15, A16, FUNCT_1: 2;

    end;

    theorem :: FACIRC_2:32

    for n be Nat holds for x,y be nonpair-yielding FinSeqLen of n holds for s be State of (n -BitAdderCirc (x,y)) holds ( Following (s,(1 + (2 * n)))) is stable

    proof

      let n be Nat, f,g be nonpair-yielding FinSeqLen of n;

      deffunc S( set, Nat) = ( BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1));

      deffunc A( set, Nat) = ( BitAdderWithOverflowCirc ((f . ($2 + 1)),(g . ($2 + 1)),$1));

      deffunc o( set, Nat) = ( MajorityOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1));

      set S0 = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

      set A0 = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE )));

      set N = ((1,2) followed_by ( In (n, NAT )));



       A1: (N . 0 ) = 1 by FUNCT_7: 122;



       A2: (N . 1) = 2 by FUNCT_7: 123;



       A3: (N . 2) = n by FUNCT_7: 124;

      deffunc n( Element of NAT ) = (N . $1);



       A4: for x be set, n be Nat holds A(x,n) is Boolean gate`2=den strict Circuit of S(x,n);

       A5:

      now

        let s be State of A0;

        ( Following (s,1)) = ( Following s) by FACIRC_1: 14;

        hence ( Following (s, n(0))) is stable by A1, CIRCCMB2: 2;

      end;

      deffunc F( Element of NAT ) = ($1 -BitMajorityOutput (f,g));

      consider h be ManySortedSet of NAT such that

       A6: for n be Element of NAT holds (h . n) = F(n) from PBOOLE:sch 5;



       A7: for n be Nat, x be set holds for A be non-empty Circuit of S(x,n) st x = (h . n) & A = A(x,n) holds for s be State of A holds ( Following (s, n())) is stable

      proof

        let n be Nat, x be set, A be non-empty Circuit of S(x,n);



         A8: n in NAT by ORDINAL1:def 12;

        assume x = (h . n);

        then

         A9: x = (n -BitMajorityOutput (f,g)) by A6, A8;

        then

         A10: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, '&' ] by Th25;

        x <> [ <*(f . (n + 1)), (g . (n + 1))*>, 'xor' ] by A9, Th25;

        hence thesis by A2, A10, Th31;

      end;

      set Sn = (n -BitAdderStr (f,g));

      set An = (n -BitAdderCirc (f,g));

      set o0 = ( 0 -BitMajorityOutput (f,g));

      consider f1,g1,h1 be ManySortedSet of NAT such that

       A11: (n -BitAdderStr (f,g)) = (f1 . n) and

       A12: (n -BitAdderCirc (f,g)) = (g1 . n) and

       A13: (f1 . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A14: (g1 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> FALSE ))) and

       A15: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] and

       A16: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for z be set st S = (f1 . n) & A = (g1 . n) & z = (h1 . n) holds (f1 . (n + 1)) = (S +* ( BitAdderWithOverflowStr ((f . (n + 1)),(g . (n + 1)),z))) & (g1 . (n + 1)) = (A +* ( BitAdderWithOverflowCirc ((f . (n + 1)),(g . (n + 1)),z))) & (h1 . (n + 1)) = ( MajorityOutput ((f . (n + 1)),(g . (n + 1)),z)) by Def4;

      now

        let i be object;

        assume i in NAT ;

        then

        reconsider j = i as Element of NAT ;



        thus (h1 . i) = (j -BitMajorityOutput (f,g)) by A13, A14, A15, A16, Th6

        .= (h . i) by A6;

      end;

      then

       A17: h1 = h by PBOOLE: 3;



       A18: ex u,v be ManySortedSet of NAT st Sn = (u . n()) & An = (v . n()) & (u . 0 ) = S0 & (v . 0 ) = A0 & (h . 0 ) = o0 & for n be Nat, S be non empty ManySortedSign, A1 be non-empty MSAlgebra over S holds for x be set, A2 be non-empty MSAlgebra over S(x,n) st S = (u . n) & A1 = (v . n) & x = (h . n) & A2 = A(x,n) holds (u . (n + 1)) = (S +* S(x,n)) & (v . (n + 1)) = (A1 +* A2) & (h . (n + 1)) = o(x,n)

      proof

        take f1, g1;

        thus thesis by A3, A6, A11, A12, A13, A14, A16, A17;

      end;



       A19: ( InnerVertices S0) is Relation & ( InputVertices S0) is without_pairs by FACIRC_1: 38, FACIRC_1: 39;



       A20: [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )] = o0 by Th7;

      ( InnerVertices S0) = { [ <*> , (( 0 -tuples_on BOOLEAN ) --> FALSE )]} by CIRCCOMB: 42;

      then

       A21: (h . 0 ) = o0 & o0 in ( InnerVertices S0) by A6, A20, TARSKI:def 1;



       A22: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation by FACIRC_1: 88;



       A23: for n be Nat, x be set st x = (h . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs

      proof

        let n be Nat, x be set such that

         A24: x = (h . n);

        n in NAT by ORDINAL1:def 12;

        then

         A25: x = (n -BitMajorityOutput (f,g)) by A6, A24;

        then

         A26: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, '&' ] by Th25;

        x <> [ <*(f . (n + 1)), (g . (n + 1))*>, 'xor' ] by A25, Th25;

        then

         A27: ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A26, Th22;

        let a be pair object;

        assume

         A28: a in (( InputVertices S(x,n)) \ {x});

        then

         A29: a in {(f . (n + 1)), (g . (n + 1)), x} by A27, XBOOLE_0:def 5;



         A30: not a in {x} by A28, XBOOLE_0:def 5;

        a = (f . (n + 1)) or a = (g . (n + 1)) or a = x by A29, ENUMSET1:def 1;

        hence thesis by A30, TARSKI:def 1;

      end;



       A31: for n be Nat, x be set st x = (h . n) holds (h . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n))

      proof

        let n be Nat, x be set such that

         A32: x = (h . n);

        n in NAT by ORDINAL1:def 12;

        then

         A33: x = (n -BitMajorityOutput (f,g)) by A6, A32;

        (h . (n + 1)) = ((n + 1) -BitMajorityOutput (f,g)) by A6;

        hence (h . (n + 1)) = o(x,n) by A33, Th12;



         A34: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, '&' ] by A33, Th25;

        x <> [ <*(f . (n + 1)), (g . (n + 1))*>, 'xor' ] by A33, Th25;

        then ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A34, Th22;

        hence x in ( InputVertices S(x,n)) by ENUMSET1:def 1;

        set xx = (f . (n + 1)), xy = (g . (n + 1));



         A35: o(x,n) in { o(x,n)} by TARSKI:def 1;

        ( InnerVertices S(x,n)) = (( { [ <*xx, xy*>, 'xor' ], ( 2GatesCircOutput (xx,xy,x, 'xor' ))} \/ { [ <*xx, xy*>, '&' ], [ <*xy, x*>, '&' ], [ <*x, xx*>, '&' ]}) \/ {( MajorityOutput (xx,xy,x))}) by Th23;

        hence thesis by A35, XBOOLE_0:def 3;

      end;

      for s be State of An holds ( Following (s,( n(0) + ( n() * n())))) is stable from CIRCCMB2:sch 22( A4, A5, A7, A18, A19, A21, A22, A23, A31);

      hence thesis by A1, A2, A3;

    end;

    theorem :: FACIRC_2:33

    for i be Nat, x be FinSeqLen of (i + 1) holds ex y be FinSeqLen of i, a be object st x = (y ^ <*a*>) by Lm1;

    theorem :: FACIRC_2:34

    for i be Nat, x be nonpair-yielding FinSeqLen of (i + 1) holds ex y be nonpair-yielding FinSeqLen of i, a be non pair set st x = (y ^ <*a*>) by Lm2;