fscirc_2.miz



    begin

    definition

      let n be Nat;

      let x,y be FinSequence;

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

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

      

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

      :: FSCIRC_2:def1

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

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

      uniqueness

      proof

        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 ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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 ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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

        deffunc S( set, Nat) = ( BitSubtracterWithBorrowStr ((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 ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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;

      :: FSCIRC_2:def2

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

      : Def2: ex f,g,h be ManySortedSet of NAT st (n -BitSubtracterStr (x,y)) = (f . n) & it = (g . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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 +* ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),z));

      uniqueness

      proof

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

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

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

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

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

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

        deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitSubtracterWithBorrowCirc ((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 Sn 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 ) --> TRUE )));

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

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

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

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

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

        deffunc A( non empty ManySortedSign, non-empty MSAlgebra over $1, set, Nat) = ($2 +* ( BitSubtracterWithBorrowCirc ((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 (n -BitSubtracterStr (x,y)) = (f . n) & (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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 Def1;

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

      :: FSCIRC_2:def3

      func n -BitBorrowOutput (x,y) -> Element of ( InnerVertices (n -BitSubtracterStr (x,y))) means

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

      uniqueness

      proof

        let o1,o2 be Element of ( InnerVertices (n -BitSubtracterStr (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 holds (h1 . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)));

        given h2 be ManySortedSet of NAT such that

         A4: o2 = (h2 . n) and

         A5: (h2 . 0 ) = c and

         A6: for n be Nat holds (h2 . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h2 . n)));

        deffunc F( Nat, set) = ( BorrowOutput ((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 +* ( BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2)));

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

        consider f,g be ManySortedSet of NAT such that

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

         A14: (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 Def1;

        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 ) --> TRUE )))) = {c} by CIRCCOMB: 42;

        then c in ( InnerVertices ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE )))) 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;

          ( BorrowOutput ((x . (i + 1)),(y . (i + 1)),(g . i))) in ( InnerVertices ( BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(g . i)))) by FACIRC_1: 21;

          then

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

          

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

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

          hence contradiction by A20, A22, A23;

        end;

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

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

        then

        reconsider o = (g . n) as Element of ( InnerVertices (n -BitSubtracterStr (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 :: FSCIRC_2:1

    

     Th1: for x,y be FinSequence, f,g,h be ManySortedSet of NAT st (f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] & 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 +* ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),z)) holds for n be Nat holds (n -BitSubtracterStr (x,y)) = (f . n) & (n -BitSubtracterCirc (x,y)) = (g . n) & (n -BitBorrowOutput (x,y)) = (h . n)

    proof

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

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

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

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

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

      assume that

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

       A2: (h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] 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 -BitSubtracterStr (x,y)) = (f1 . n) and

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

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

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

       A8: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] 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 Def2;

      

       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 -BitSubtracterStr (x,y)) = (f . n) & (n -BitSubtracterCirc (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 ) --> TRUE ))) 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 ) --> TRUE )] 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 -BitBorrowOutput (x,y)) = (h1 . n) and

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

       A21: for n be Nat holds (h1 . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n))) by Def3;

      

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

      

       A23: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] 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 :: FSCIRC_2:2

    

     Th2: for a,b be FinSequence holds ( 0 -BitSubtracterStr (a,b)) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & ( 0 -BitSubtracterCirc (a,b)) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) & ( 0 -BitBorrowOutput (a,b)) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )]

    proof

      let a,b be FinSequence;

      

       A1: ex f,g,h be ManySortedSet of NAT st (( 0 -BitSubtracterStr (a,b)) = (f . 0 )) & (( 0 -BitSubtracterCirc (a,b)) = (g . 0 )) & ((f . 0 ) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE )))) & ((g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE )))) & ((h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )]) & (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 +* ( BitSubtracterWithBorrowStr ((a . (n + 1)),(b . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((a . (n + 1)),(b . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((a . (n + 1)),(b . (n + 1)),z))) by Def2;

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

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

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

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FSCIRC_2:3

    

     Th3: for a,b be FinSequence, c be set st c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] holds (1 -BitSubtracterStr (a,b)) = (( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) +* ( BitSubtracterWithBorrowStr ((a . 1),(b . 1),c))) & (1 -BitSubtracterCirc (a,b)) = (( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) +* ( BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c))) & (1 -BitBorrowOutput (a,b)) = ( BorrowOutput ((a . 1),(b . 1),c))

    proof

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

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

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

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

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

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

       A5: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 +* ( BitSubtracterWithBorrowStr ((a . (n + 1)),(b . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((a . (n + 1)),(b . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((a . (n + 1)),(b . (n + 1)),z)) by A1, Def2;

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

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

    end;

    theorem :: FSCIRC_2:4

    for a,b,c be set st c = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] holds (1 -BitSubtracterStr ( <*a*>, <*b*>)) = (( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) +* ( BitSubtracterWithBorrowStr (a,b,c))) & (1 -BitSubtracterCirc ( <*a*>, <*b*>)) = (( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) +* ( BitSubtracterWithBorrowCirc (a,b,c))) & (1 -BitBorrowOutput ( <*a*>, <*b*>)) = ( BorrowOutput (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, Th3;

    end;

    theorem :: FSCIRC_2:5

    

     Th5: for n be Nat holds for p,q be FinSeqLen of n holds for p1,p2,q1,q2 be FinSequence holds (n -BitSubtracterStr ((p ^ p1),(q ^ q1))) = (n -BitSubtracterStr ((p ^ p2),(q ^ q2))) & (n -BitSubtracterCirc ((p ^ p1),(q ^ q1))) = (n -BitSubtracterCirc ((p ^ p2),(q ^ q2))) & (n -BitBorrowOutput ((p ^ p1),(q ^ q1))) = (n -BitBorrowOutput ((p ^ p2),(q ^ q2)))

    proof

      let n be Nat;

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

      let p,q be FinSeqLen of n;

      let p1,p2,q1,q2 be FinSequence;

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

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

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

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

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

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

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

       A4: (g1 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 Def2;

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

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

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

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

       A10: (g2 . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 +* ( BitSubtracterWithBorrowStr (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z))) & (g2 . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z))) & (h2 . (n + 1)) = ( BorrowOutput (((p ^ p2) . (n + 1)),((q ^ q2) . (n + 1)),z)) by Def2;

      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)) = ( BorrowOutput (((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 +* ( BitSubtracterWithBorrowStr (((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 +* ( BitSubtracterWithBorrowCirc (((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 -BitSubtracterStr ((p ^ p1),(q ^ q1))) = (n -BitSubtracterStr ((p ^ p2),(q ^ q2))) & (n -BitSubtracterCirc ((p ^ p1),(q ^ q1))) = (n -BitSubtracterCirc ((p ^ p2),(q ^ q2))) by A1, A2, A7, A8;

      

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

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

      hence thesis by A31, A32;

    end;

    theorem :: FSCIRC_2:6

    for n be Element of NAT holds for x,y be FinSeqLen of n holds for a,b be set holds ((n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>))) = ((n -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y))))) & ((n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>))) = ((n -BitSubtracterCirc (x,y)) +* ( BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y))))) & ((n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>))) = ( BorrowOutput (a,b,(n -BitBorrowOutput (x,y))))

    proof

      let n be Element of NAT ;

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

      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 -BitSubtracterStr (p,q)) = (f . n) and

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

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

       A4: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 +* ( BitSubtracterWithBorrowStr ((p . (n + 1)),(q . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((p . (n + 1)),(q . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((p . (n + 1)),(q . (n + 1)),z)) by Def2;

      

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

      

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

      

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

      

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

      

       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 -BitSubtracterStr (p,q)) = (n -BitSubtracterStr (x,y)) by A15, Th5;

      

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

      (n -BitBorrowOutput (p,q)) = (n -BitBorrowOutput (x,y)) by A15, A16, Th5;

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

    end;

    theorem :: FSCIRC_2:7

    

     Th7: for n be Nat holds for x,y be FinSequence holds ((n + 1) -BitSubtracterStr (x,y)) = ((n -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))) & ((n + 1) -BitSubtracterCirc (x,y)) = ((n -BitSubtracterCirc (x,y)) +* ( BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))) & ((n + 1) -BitBorrowOutput (x,y)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))

    proof

      let n be Nat;

      let x,y be FinSequence;

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

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

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

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

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

       A4: (g . 0 ) = ( 1GateCircuit ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) 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 +* ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),z))) & (g . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),z))) & (h . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),z)) by Def2;

      

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

      

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

      

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

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

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

    end;

    theorem :: FSCIRC_2:8

    

     Th8: for n,m be Nat st n <= m holds for x,y be FinSequence holds ( InnerVertices (n -BitSubtracterStr (x,y))) c= ( InnerVertices (m -BitSubtracterStr (x,y)))

    proof

      let n,m be 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;

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

      

       A3: L[ 0 ];

      

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

      proof

        let j be Nat;

        assume

         A5: ( InnerVertices (n -BitSubtracterStr (x,y))) c= ( InnerVertices ((n + j) -BitSubtracterStr (x,y)));

        

         A6: ( InnerVertices (n -BitSubtracterStr (x,y))) c= (( InnerVertices (n -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))) by XBOOLE_1: 7;

        (( InnerVertices (n -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))) c= (( InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))) by A5, XBOOLE_1: 9;

        then ( InnerVertices (n -BitSubtracterStr (x,y))) c= (( InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))) by A6;

        then ( InnerVertices (n -BitSubtracterStr (x,y))) c= ( InnerVertices (((n + j) -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))) by FACIRC_1: 27;

        hence thesis by Th7;

      end;

      

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

      m = (n + i) by A2;

      hence thesis by A7;

    end;

    theorem :: FSCIRC_2:9

    for n be Element of NAT holds for x,y be FinSequence holds ( InnerVertices ((n + 1) -BitSubtracterStr (x,y))) = (( InnerVertices (n -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))))))

    proof

      let n be Element of NAT ;

      let x,y be FinSequence;

      ( InnerVertices ((n -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))) = (( InnerVertices (n -BitSubtracterStr (x,y))) \/ ( InnerVertices ( BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))) by FACIRC_1: 27;

      hence thesis by Th7;

    end;

    definition

      let k,n be Nat;

      let x,y be FinSequence;

      :: FSCIRC_2:def4

      func (k,n) -BitSubtracterOutput (x,y) -> Element of ( InnerVertices (n -BitSubtracterStr (x,y))) means

      : Def4: ex i be Element of NAT st k = (i + 1) & it = ( BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))));

      uniqueness ;

      existence

      proof

        consider i be Nat such that

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

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

        set o = ( BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))));

        

         A4: ( InnerVertices (k -BitSubtracterStr (x,y))) c= ( InnerVertices (n -BitSubtracterStr (x,y))) by A2, Th8;

        

         A5: o in ( InnerVertices ( BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))) by A3, FACIRC_1: 21;

        

         A6: (k -BitSubtracterStr (x,y)) = ((i -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))) by A3, Th7;

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

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

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

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

        hence thesis by A3, A4;

      end;

    end

    theorem :: FSCIRC_2:10

    for n,k be Element of NAT st k < n holds for x,y be FinSequence holds (((k + 1),n) -BitSubtracterOutput (x,y)) = ( BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (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) -BitSubtracterOutput (x,y)) = ( BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(i -BitBorrowOutput (x,y))))) by A2, Def4;

      hence thesis;

    end;

    theorem :: FSCIRC_2:11

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

    proof

      let n be Element of NAT ;

      let x,y be FinSequence;

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

      ( 0 -BitSubtracterStr (x,y)) = ( 1GateCircStr ( <*> ,(( 0 -tuples_on BOOLEAN ) --> TRUE ))) by Th2;

      then

       A1: P[ 0 ] by FACIRC_1: 38;

       A2:

      now

        let i be Nat;

        assume

         A3: P[i];

        

         A4: ((i + 1) -BitSubtracterStr (x,y)) = ((i -BitSubtracterStr (x,y)) +* ( BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))) by Th7;

        ( InnerVertices ( BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))) is Relation by FSCIRC_1: 22;

        hence P[(i + 1)] 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 :: FSCIRC_2:12

    

     Th12: for x,y,c be set holds ( InnerVertices ( BorrowIStr (x,y,c))) = { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]}

    proof

      let x,y,c be set;

      

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

      

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

      ( InnerVertices ( BorrowIStr (x,y,c))) = (( InnerVertices (( 1GateCircStr ( <*x, y*>, and2a )) +* ( 1GateCircStr ( <*y, c*>, and2 )))) \/ ( InnerVertices ( 1GateCircStr ( <*x, c*>, and2a )))) by A1, CIRCCOMB: 11

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: FSCIRC_2:13

    

     Th13: for x,y,c be set st x <> [ <*y, c*>, and2 ] & y <> [ <*x, c*>, and2a ] & c <> [ <*x, y*>, and2a ] holds ( InputVertices ( BorrowIStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be set;

      assume that

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

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

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

      

       A4: ( 1GateCircStr ( <*x, y*>, and2a )) tolerates ( 1GateCircStr ( <*y, c*>, and2 )) 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*>, and2 }} by TARSKI:def 2;

      then

       A13: y <> [ <*y, c*>, and2 ] 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*>, and2 ] 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*>, and2a }} by TARSKI:def 2;

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

      then

       A21: not [ <*x, y*>, and2a ] 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*>, and2a }} by TARSKI:def 2;

      then

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

      

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

      

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

      

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

      

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

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

      then

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

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

      then

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

      

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

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

      then

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

      

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

      

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

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

      then

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

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

      then

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

      

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

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

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

      then

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

      ( InputVertices ( BorrowIStr (x,y,c))) = ((( InputVertices (( 1GateCircStr ( <*x, y*>, and2a )) +* ( 1GateCircStr ( <*y, c*>, and2 )))) \ ( InnerVertices ( 1GateCircStr ( <*x, c*>, and2a )))) \/ (( InputVertices ( 1GateCircStr ( <*x, c*>, and2a ))) \ ( InnerVertices (( 1GateCircStr ( <*x, y*>, and2a )) +* ( 1GateCircStr ( <*y, c*>, and2 )))))) by CIRCCMB2: 5, CIRCCOMB: 47

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

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

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

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

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

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

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

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

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

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

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

      .= ((( {x, y} \/ ( {y, c} \ { [ <*x, y*>, and2a ]})) \ { [ <*x, c*>, and2a ]}) \/ ( {x, c} \ { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ]})) by A1, A13, FACIRC_2: 1

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

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

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

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

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

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

      .= ( {x, y, c} \/ {x, c}) 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 :: FSCIRC_2:14

    

     Th14: for x,y,c be set holds ( InnerVertices ( BorrowStr (x,y,c))) = ( { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} \/ {( BorrowOutput (x,y,c))})

    proof

      let x,y,c be set;

      set xy = [ <*x, y*>, and2a ], yc = [ <*y, c*>, and2 ], xc = [ <*x, c*>, and2a ];

      set Cxy = ( 1GateCircStr ( <*x, y*>, and2a )), Cyc = ( 1GateCircStr ( <*y, c*>, and2 )), Cxc = ( 1GateCircStr ( <*x, c*>, and2a )), Cxyc = ( 1GateCircStr ( <* [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]*>, or3 ));

      

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

      

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

      

       A3: Cxc tolerates Cxyc by CIRCCOMB: 47;

      

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

      

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

      

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

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

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

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

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

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

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

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

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

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

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

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

    end;

    theorem :: FSCIRC_2:15

    

     Th15: for x,y,c be set st x <> [ <*y, c*>, and2 ] & y <> [ <*x, c*>, and2a ] & c <> [ <*x, y*>, and2a ] holds ( InputVertices ( BorrowStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be set;

      set xy = [ <*x, y*>, and2a ], yc = [ <*y, c*>, and2 ], xc = [ <*x, c*>, and2a ];

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

      

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

      

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

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

      set BI = ( BorrowIStr (x,y,c));

      assume that

       A3: x <> yc and

       A4: y <> xc and

       A5: c <> xy;

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

      then

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

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

      then

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

      then

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

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

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

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

      then

       A9: ( the_rank_of xc) in ( the_rank_of [ <*xy, yc, xc*>, 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, xc*>) by A7, FINSEQ_1: 1;

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

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

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

      then

       A12: ( the_rank_of xy) in ( the_rank_of [ <*xy, yc, xc*>, 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, xc*>) by A7, FINSEQ_1: 1;

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

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

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

      then

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

      

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

      

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

      proof

        thus ( {x, y, c} \ { [ <*xy, yc, xc*>, 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, xc*>, or3 ] by A6, A9, A10, A12, A13, A15, CLASSES1: 82;

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

        hence thesis by A18, XBOOLE_0:def 5;

      end;

      

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

      .= ( {x, y, c} \/ ( {xy, yc, xc} \ ( InnerVertices BI))) by A1, A2, A3, A4, A5, A17, Th13

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

      .= {x, y, c};

    end;

    theorem :: FSCIRC_2:16

    

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

    proof

      let x,y,c be set such that

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

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

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

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

      

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

      ( InputVertices ( BorrowStr (x,y,c))) = {x, y, c} by A1, A2, A3, Th15;

      hence thesis by A5, CIRCCOMB: 47, FACIRC_2: 21;

    end;

    theorem :: FSCIRC_2:17

    

     Th17: for x,y,c be set holds ( InnerVertices ( BitSubtracterWithBorrowStr (x,y,c))) = (( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]}) \/ {( BorrowOutput (x,y,c))})

    proof

      let x,y,c be set;

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

      

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

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

      .= ( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ ( { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} \/ {( BorrowOutput (x,y,c))})) by Th14

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

      hence thesis;

    end;

    registration

      let n be Nat;

      let x,y be FinSequence;

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

      coherence

      proof

        

         A1: ex h be ManySortedSet of NAT st (( 0 -BitBorrowOutput (x,y)) = (h . 0 )) & ((h . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )]) & (for n be Nat holds (h . (n + 1)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)))) by Def3;

        defpred P[ Nat] means ($1 -BitBorrowOutput (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) -BitBorrowOutput (x,y)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) by Th7

          .= [ <* [ <*(x . (n + 1)), (y . (n + 1))*>, and2a ], [ <*(y . (n + 1)), (n -BitBorrowOutput (x,y))*>, and2 ], [ <*(x . (n + 1)), (n -BitBorrowOutput (x,y))*>, and2a ]*>, or3 ];

          hence thesis;

        end;

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

        hence thesis;

      end;

    end

    theorem :: FSCIRC_2:18

    

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

    proof

      let x,y be FinSequence;

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

      

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

      ( 0 -BitBorrowOutput (x,y)) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] by Th2;

      then

       A2: P[ 0 ] by A1;

       A3:

      now

        let n be Nat;

        assume P[n];

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

        

         A4: ((n + 1) -BitBorrowOutput (x,y)) = ( BorrowOutput ((x . (n + 1)),(y . (n + 1)),c)) by Th7

        .= [ <* [ <*(x . (n + 1)), (y . (n + 1))*>, and2a ], [ <*(y . (n + 1)), c*>, and2 ], [ <*(x . (n + 1)), c*>, and2a ]*>, 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 i be Nat holds P[i] from NAT_1:sch 2( A2, A3);

    end;

    theorem :: FSCIRC_2:19

    

     Th19: for n be Nat, x,y be FinSequence, p be set holds (n -BitBorrowOutput (x,y)) <> [p, and2 ] & (n -BitBorrowOutput (x,y)) <> [p, and2a ] & (n -BitBorrowOutput (x,y)) <> [p, 'xor' ]

    proof

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

      

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

      

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

      

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

      

       A4: ( proj1 ( [p, and2 ] `2 )) = (2 -tuples_on BOOLEAN ) by A1;

      

       A5: ( proj1 ( [p, and2a ] `2 )) = (2 -tuples_on BOOLEAN ) by A2;

      

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

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

      hence thesis by A4, A5, A6, FINSEQ_2: 110;

    end;

    theorem :: FSCIRC_2:20

    

     Th20: for f,g be nonpair-yielding FinSequence holds for n be Nat holds ( InputVertices ((n + 1) -BitSubtracterStr (f,g))) = (( InputVertices (n -BitSubtracterStr (f,g))) \/ (( InputVertices ( BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput (f,g))))) \ {(n -BitBorrowOutput (f,g))})) & ( InnerVertices (n -BitSubtracterStr (f,g))) is Relation & ( InputVertices (n -BitSubtracterStr (f,g))) is without_pairs

    proof

      let f,g be nonpair-yielding FinSequence;

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

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

      deffunc F( Nat) = ($1 -BitBorrowOutput (f,g));

      consider h be ManySortedSet of NAT such that

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

      

       A2: for n be Nat holds (h . n) = F(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) = ( BorrowOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1));

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

      

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

      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 -BitBorrowOutput (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 FSCIRC_1: 22;

       A8:

      now

        let n be Element of NAT , x be set such that

         A9: x = h(n);

        

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

        then

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

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

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

      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 such that

         A13: x = h(n);

        n in NAT by ORDINAL1:def 12;

        then

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

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

        proof

          let a be pair object;

          assume

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

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

          then

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

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

          hence contradiction by A16, TARSKI:def 1;

        end;

      end;

       A17:

      now

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

        

         A18: n in NAT by ORDINAL1:def 12;

        assume that

         A19: S = Sn(n) and

         A20: x = (h . n);

        

         A21: x = (n -BitBorrowOutput (f,g)) by A2, A20;

        

         A22: h(+) = ((n + 1) -BitBorrowOutput (f,g)) by A2;

        thus Sn(+) = (S +* S(x,n)) by A19, A21, Th7;

        thus (h . (n + 1)) = o(x,n) by A21, A22, Th7;

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

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

        

         A23: ( 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))*>, and2a ], [ <*(g . (n + 1)), x*>, and2 ], [ <*(f . (n + 1)), x*>, and2a ]}) \/ {( BorrowOutput ((f . (n + 1)),(g . (n + 1)),x))}) by Th17;

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

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

      end;

      

       A24: 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, A17);

      let n be Nat;

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

      hence thesis by A24;

    end;

    theorem :: FSCIRC_2:21

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

    proof

      defpred P[ Nat] means for x,y be nonpair-yielding FinSeqLen of $1 holds ( InputVertices ($1 -BitSubtracterStr (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 ) --> TRUE );

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

        

        hence ( InputVertices ( 0 -BitSubtracterStr (x,y))) = ( rng <*> ) by CIRCCOMB: 42

        .= (( rng x) \/ ( rng y));

      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 FACIRC_2: 34;

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

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

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

        

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

        then

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

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

        

        then

         A8: (x . (i + 1)) = ( <*z1*> . 1) by A4, A7, FINSEQ_1:def 7

        .= z1 by FINSEQ_1:def 8;

        

         A9: 1 in ( dom <*z2*>) by A6, FINSEQ_1:def 8;

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

        

        then

         A10: (y . (i + 1)) = ( <*z2*> . 1) by A5, A9, FINSEQ_1:def 7

        .= z2 by FINSEQ_1:def 8;

        

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

        

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

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

        

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

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

        

         A14: (i -BitBorrowOutput (x,y)) <> [ <*z1, z2*>, and2a ] by Th19;

        

         A15: (i -BitBorrowOutput (x,y)) <> [ <*z1, z2*>, 'xor' ] by Th19;

        

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

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

        then (i -BitSubtracterStr (x,y)) = (i -BitSubtracterStr (x9,y9)) by A4, A5, A16, Th5;

        

        hence ( InputVertices S) = (( InputVertices (i -BitSubtracterStr (x9,y9))) \/ (( InputVertices ( BitSubtracterWithBorrowStr (z1,z2,(i -BitBorrowOutput (x,y))))) \ {(i -BitBorrowOutput (x,y))})) by A8, A10, Th20

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

        .= ((( rng x9) \/ ( rng y9)) \/ ( {z1, z2, (i -BitBorrowOutput (x,y))} \ {(i -BitBorrowOutput (x,y))})) by A14, A15, Th16

        .= ((( rng x9) \/ ( rng y9)) \/ {z1, z2}) by A11, 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 A12, A13, XBOOLE_1: 4;

      end;

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

    end;

    

     Lm1: for x,y,c be set holds for s be State of ( BorrowCirc (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*>, and2a ]) = (( 'not' a1) '&' a2) & (( Following s) . [ <*y, c*>, and2 ]) = (a2 '&' a3) & (( Following s) . [ <*x, c*>, and2a ]) = (( 'not' a1) '&' a3)

    proof

      let x,y,c be set;

      let s be State of ( BorrowCirc (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 = ( BorrowStr (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 FSCIRC_1: 6;

      

       A7: y in the carrier of S by FSCIRC_1: 6;

      

       A8: c in the carrier of S by FSCIRC_1: 6;

       [ <*x, y*>, and2a ] in ( InnerVertices ( BorrowStr (x,y,c))) by FSCIRC_1: 7;

      

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

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

      .= (( 'not' a1) '&' a2) by TWOSCOMP:def 2;

       [ <*y, c*>, and2 ] in ( InnerVertices ( BorrowStr (x,y,c))) by FSCIRC_1: 7;

      

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

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

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

       [ <*x, c*>, and2a ] in ( InnerVertices ( BorrowStr (x,y,c))) by FSCIRC_1: 7;

      

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

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

      .= (( 'not' a1) '&' a3) by TWOSCOMP:def 2;

    end;

    theorem :: FSCIRC_2:22

    

     Th22: for x,y,c be set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, and2a ]) & a2 = (s . [ <*y, c*>, and2 ]) & a3 = (s . [ <*x, c*>, and2a ]) holds (( Following s) . ( BorrowOutput (x,y,c))) = ((a1 'or' a2) 'or' a3)

    proof

      let x,y,c be set;

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

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

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

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

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

      set xy = [ <*x, y*>, and2a ], yc = [ <*y, c*>, and2 ], cx = [ <*x, c*>, and2a ];

      set S = ( BorrowStr (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 FSCIRC_1: 7;

      

      thus (( Following s) . ( BorrowOutput (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;

    

     Lm2: for x,y,c be set st x <> [ <*y, c*>, and2 ] & y <> [ <*x, c*>, and2a ] & c <> [ <*x, y*>, and2a ] holds for s be State of ( BorrowCirc (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)) . ( BorrowOutput (x,y,c))) = (((( 'not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (( 'not' a1) '&' a3)) & (( Following (s,2)) . [ <*x, y*>, and2a ]) = (( 'not' a1) '&' a2) & (( Following (s,2)) . [ <*y, c*>, and2 ]) = (a2 '&' a3) & (( Following (s,2)) . [ <*x, c*>, and2a ]) = (( 'not' a1) '&' a3)

    proof

      let x,y,c be set such that

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

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

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

      let s be State of ( BorrowCirc (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*>, and2a ], yc = [ <*y, c*>, and2 ], cx = [ <*x, c*>, and2a ];

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

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

      

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

      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) = (( 'not' a1) '&' a2) by A4, A5, A6, Lm1;

      

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

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

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

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

    end;

    theorem :: FSCIRC_2:23

    

     Th23: for x,y,c be set st x <> [ <*y, c*>, and2 ] & y <> [ <*x, c*>, and2a ] & c <> [ <*x, y*>, and2a ] holds for s be State of ( BorrowCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be set;

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

      assume that

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

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

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

      let s be State of ( BorrowCirc (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 FSCIRC_1: 6;

      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 . ( BorrowOutput (x,y,c))) = (((( 'not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (( 'not' a1) '&' a3)) by A1, A2, A3, Lm2;

      

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

      

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

      

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

      

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

      

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

      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*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} \/ {( BorrowOutput (x,y,c))}) by Th14;

            then v in { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} or v in {( BorrowOutput (x,y,c))} by XBOOLE_0:def 3;

            then v = [ <*x, y*>, and2a ] or v = [ <*y, c*>, and2 ] or v = [ <*x, c*>, and2a ] or v = ( BorrowOutput (x,y,c)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A9, A10, A11, A12, A21, A22, A23, Lm1, Th22;

          end;

        end;

      end;

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

    end;

    theorem :: FSCIRC_2:24

    for x,y,c be set st x <> [ <*y, c*>, and2 ] & y <> [ <*x, c*>, and2a ] & c <> [ <*x, y*>, and2a ] & c <> [ <*x, y*>, 'xor' ] holds for s be State of ( BitSubtracterWithBorrowCirc (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)) . ( BitSubtracterOutput (x,y,c))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . ( BorrowOutput (x,y,c))) = (((( 'not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (( 'not' a1) '&' a3))

    proof

      let x,y,c be set such that

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

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

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

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

      set f = 'xor' ;

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

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

      set A1 = ( BitSubtracterCirc (x,y,c)), A2 = ( BorrowCirc (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 FSCIRC_1: 6;

      

       A12: y in the carrier of S2 by FSCIRC_1: 6;

      

       A13: c in the carrier of S2 by FSCIRC_1: 6;

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

      

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

      

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

      

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

      

       A17: ( InnerVertices S1) misses ( InputVertices S2) by A4, A14, A15, FACIRC_1: 57;

      

       A18: ( InnerVertices S2) misses ( InputVertices S1) by A4, A14, A16, FACIRC_1: 57;

      

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

      then

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

      

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

      

       A22: a3 = (s1 . c) by A7, A10, A19, FUNCT_1: 47;

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

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

      

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

      then

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

      

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

      

       A26: a3 = (s2 . c) by A7, A13, A23, FUNCT_1: 47;

      (( Following (t,2)) . ( BorrowOutput (x,y,c))) = (( Following (s2,2)) . ( BorrowOutput (x,y,c))) by A17, FACIRC_1: 33;

      hence thesis by A1, A2, A3, A24, A25, A26, Lm2;

    end;

    theorem :: FSCIRC_2:25

    

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

    proof

      let x,y,c be set such that

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

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

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

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

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

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

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

      set A1 = ( BitSubtracterCirc (x,y,c)), A2 = ( BorrowCirc (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);

      

       A5: ( InputVertices S2) = {x, y, c} by A1, A2, A3, Th15;

      

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

      

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

      

       A8: ( InnerVertices S1) misses ( InputVertices S2) by A4, A5, A6, FACIRC_1: 57;

      

       A9: ( InnerVertices S2) misses ( InputVertices S1) by A4, A5, A7, FACIRC_1: 57;

      then

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

      

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

      

       A12: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) by A8, FACIRC_1: 31;

      

       A13: ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A8, FACIRC_1: 31;

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

      

      then

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

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

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

      

      then

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

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

      

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

      

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

      

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

      

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

      

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

      

       A21: 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 A21, 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 A10, A11, A12, A13, A14, A15, A19, A20, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A14, A15, FACIRC_1: 12;

      end;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A16, A17, A18, FUNCT_1: 2;

    end;

    theorem :: FSCIRC_2:26

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

    proof

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

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

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

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

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

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

      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 -BitBorrowOutput (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 -BitBorrowOutput (f,g)) by A6, A8;

        then

         A10: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, and2a ] by Th19;

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

        hence thesis by A2, A10, Th25;

      end;

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

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

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

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

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

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

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

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

       A15: (h1 . 0 ) = [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )] 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 +* ( BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),z))) & (g1 . (n + 1)) = (A +* ( BitSubtracterWithBorrowCirc ((f . (n + 1)),(g . (n + 1)),z))) & (h1 . (n + 1)) = ( BorrowOutput ((f . (n + 1)),(g . (n + 1)),z)) by Def2;

      now

        let i be object;

        assume i in NAT ;

        then

        reconsider j = i as Element of NAT ;

        

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

        .= (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 ) --> TRUE )] = o0 by Th2;

      ( InnerVertices S0) = { [ <*> , (( 0 -tuples_on BOOLEAN ) --> TRUE )]} 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 FSCIRC_1: 22;

      

       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 -BitBorrowOutput (f,g)) by A6, A24;

        then

         A26: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, and2a ] by Th19;

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

        then

         A27: ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A26, Th16;

        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 -BitBorrowOutput (f,g)) by A6, A32;

        (h . (n + 1)) = ((n + 1) -BitBorrowOutput (f,g)) by A6;

        hence (h . (n + 1)) = o(x,n) by A33, Th7;

        

         A34: x <> [ <*(f . (n + 1)), (g . (n + 1))*>, and2a ] by A33, Th19;

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

        then ( InputVertices S(x,n)) = {(f . (n + 1)), (g . (n + 1)), x} by A34, Th16;

        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*>, and2a ], [ <*xy, x*>, and2 ], [ <*xx, x*>, and2a ]}) \/ {( BorrowOutput (xx,xy,x))}) by Th17;

        hence thesis by A35, XBOOLE_0:def 3;

      end;

      for s be State of (n -BitSubtracterCirc (f,g)) 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;