The Mizar article:

Full Subtracter Circuit. Part II

by
Shin'nosuke Yamaguchi,
Grzegorz Bancerek, and
Katsumi Wasaki

Received February 25, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: FSCIRC_2
[ MML identifier index ]


environ

 vocabulary BOOLE, MCART_1, RELAT_1, AMI_1, CARD_1, FUNCT_1, FINSEQ_1,
      FINSEQ_2, FUNCT_4, FUNCT_5, FUNCOP_1, PBOOLE, MARGREL1, BINARITH,
      CLASSES1, PARTFUN1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, LATTICES,
      CIRCCOMB, FACIRC_1, ZF_REFLE, ZF_LANG, TWOSCOMP, FSCIRC_1, FSCIRC_2;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      MCART_1, RELAT_1, CARD_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FUNCT_5, PBOOLE, MARGREL1, BINARITH, CLASSES1, MSUALG_1, MSAFREE2,
      CIRCUIT1, CIRCUIT2, CIRCCOMB, TWOSCOMP, FACIRC_1, FACIRC_2, FSCIRC_1;
 constructors ENUMSET1, MCART_1, CLASSES1, FUNCT_5, CIRCUIT1, CIRCUIT2,
      TWOSCOMP, FSCIRC_1, BINARITH, FACIRC_2;
 clusters RELSET_1, FINSEQ_2, MARGREL1, MSUALG_1, PRE_CIRC, CIRCCOMB, FACIRC_1,
      STRUCT_0, RELAT_1, CIRCCMB2, FACIRC_2, MEMBERED, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, CIRCUIT2, FACIRC_1, XBOOLE_0;
 theorems TARSKI, AXIOMS, ZFMISC_1, ENUMSET1, MCART_1, NAT_1, RELAT_1,
      ORDINAL1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_6, PBOOLE, FUNCT_5, PRALG_1,
      CIRCUIT2, CIRCCOMB, FACIRC_1, MSAFREE2, AMI_7, CIRCCMB2, CIRCUIT1,
      TWOSCOMP, FSCIRC_1, FACIRC_2, FUNCOP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
      FINSEQ_2;
 schemes NAT_1, RECDEF_1, CIRCCMB2, PRALG_2;

begin

::------------------------------------------------------------
:: Definitions of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------

definition
 let n be Nat;
 let x,y be FinSequence;
A1:  1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE)
      is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
 func n-BitSubtracterStr(x,y) ->
      unsplit gate`1=arity gate`2isBoolean non void strict
      non empty ManySortedSign means:Def1:
  ex f,g being ManySortedSet of NAT st
   it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
   g.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
   for n being Nat, S being 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
    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);
    for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
                 strict non empty ManySortedSign st
    (ex f,h being ManySortedSet of NAT st S1 = f.n &
    f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat, S being non empty ManySortedSign, x being 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 being ManySortedSet of NAT st S2 = f.n &
    f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat, S being non empty ManySortedSign, x being 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 o(set, Nat) = BorrowOutput(x .($2+1), y.($2+1), $1);
    deffunc S(set, Nat) =
      BitSubtracterWithBorrowStr(x .($2+1), y.($2+1), $1);
    ex S being unsplit gate`1=arity gate`2isBoolean
      non void non empty non empty strict ManySortedSign,
    f,h being ManySortedSet of NAT st
    S = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat, S being non empty ManySortedSign, x being 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;
 func n-BitSubtracterCirc(x,y) ->
      Boolean gate`2=den strict Circuit of n-BitSubtracterStr(x,y)
 means :Def2:
  ex f,g,h being 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 being Nat, S being non empty ManySortedSign,
       A being non-empty MSAlgebra over S
   for z being 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 being non empty ManySortedSign, A being non-empty MSAlgebra over S
     for z being set, n being Nat holds
      A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
   thus for A1,A2 being Boolean gate`2=den strict Circuit of Sn st
   (ex f,g,h being ManySortedSet of NAT st Sn = f.n & A1 = g.n &
    f.0 = S0 & g.0 = A0 & h.0 = o0 &
    for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for x being 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 being ManySortedSet of NAT st Sn = f.n & A2 = g.n &
    f.0 = S0 & g.0 = A0 & h.0 = o0 &
    for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for x being 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 being unsplit gate`1=arity gate`2isBoolean non void strict
                non empty ManySortedSign,
        z being set, n being Nat holds S(S,z,n)
      is unsplit gate`1=arity gate`2isBoolean non void strict;
A3:  for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
                   non empty ManySortedSign,
         A being Boolean gate`2=den strict Circuit of S
     for z being set, n being 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 being non empty ManySortedSign, A being non-empty MSAlgebra over S
     for z being set, n being Nat holds
      A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
A5:  ex f,h being 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 being Nat, S being non empty ManySortedSign, z being 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 being Boolean gate`2=den strict Circuit of Sn,
       f,g,h being ManySortedSet of NAT st
    Sn = f.n & A = g.n &
    f.0 = S0 & g.0 = A0 & h.0 = o0 &
    for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for x being 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];
 func n-BitBorrowOutput(x,y) ->
      Element of InnerVertices (n-BitSubtracterStr(x,y)) means:Def3:
  ex h being ManySortedSet of NAT st
   it = h.n & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
   for n being 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 being ManySortedSet of NAT such that
A1: o1 = h1.n & h1.0 = c &
    for n being Nat holds h1.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h1.n);
   given h2 being ManySortedSet of NAT such that
A2: o2 = h2.n & h2.0 = c &
    for n being 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);
A3: dom h1 = NAT & h1.0 = c &
    for n being Nat holds h1.(n+1) = F(n,h1.n) by A1,PBOOLE:def 3;
A4: dom h2 = NAT & h2.0 = c &
    for n being Nat holds h2.(n+1) = F(n,h2.n) by A2,PBOOLE:def 3;
      h1 = h2 from LambdaRecUn(A3,A4);
   hence thesis by A1,A2;
  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 being ManySortedSet of NAT such that
A5:  n-BitSubtracterStr(x,y) = f.n & f.0 =
    1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE)
      & g.0 = c and
A6:  for n being Nat,
    S being 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 being non empty ManySortedSign st S = f.$1 &
        g.$1 in InnerVertices S;
      InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) = {c}
    by CIRCCOMB:49;
    then c in InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE)
    by TARSKI:def 1;
then A7:  P[0] by A5;
A8: for i being Nat st P[i] holds P[i+1]
    proof let i be Nat such that
A9:    ex S being non empty ManySortedSign st S = f.i & g.i in InnerVertices S
     and
A10:    for S being non empty ManySortedSign st S = f.(i+1)
       holds not g.(i+1) in InnerVertices S;
     consider S being non empty ManySortedSign such that
A11:    S = f.i & g.i in InnerVertices S by A9;
        BorrowOutput(x .(i+1), y.(i+1), g.i) in
        InnerVertices BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i)
         by FSCIRC_1:24;
      then BorrowOutput(x .(i+1), y.(i+1), g.i) in
       InnerVertices (S+*BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i)) &
      f.(i+1) = S +* BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), g.i) &
      g.(i+1) = BorrowOutput(x .(i+1), y.(i+1), g.i) by A6,A11,FACIRC_1:22;
     hence contradiction by A10;
    end;
    for i being Nat holds P[i] from Ind(A7,A8);
    then ex S being 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 A5;
   take o, g; thus o = g.n & g.0 = c by A5;
   let i be Nat;
A12: ex S being non empty ManySortedSign, x being set st
     S = f.0 & x = g.0 & P[S, x, 0] by A5;
A13: for n being Nat, S being non empty ManySortedSign, x being 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 being Nat ex S being non empty ManySortedSign st S = f.n
      & P[S,g.n,n]
     from CIRCCMB2'sch_2(A12,A6,A13);
    then ex S being non empty ManySortedSign st S = f.i;
   hence thesis by A6;
  end;
end;

::------------------------------------------------------------
:: Properties of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------

theorem Th1:
 for x,y being FinSequence, f,g,h being 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 being Nat, S being non empty ManySortedSign,
       A being non-empty MSAlgebra over S
   for z being 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)
 for n being 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 being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for z being 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 being ManySortedSet of NAT such that
A4:  n-BitSubtracterStr(x,y) = f1.n & n-BitSubtracterCirc(x,y) = g1.n and
A5:  f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
A6:  for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for z being 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;
A7: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S st
     S = f.0 & A = g.0 by A1;
A8: f.0 = f1.0 & g.0 = g1.0 & h.0 = h1.0 by A1,A2,A5;
A9: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
     for z being set, n being 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(A7,A8,A3,A6,A9);
   hence n-BitSubtracterStr(x,y) = f.n & n-BitSubtracterCirc(x,y) = g.n by A4;
A10:  for n being Nat, S being non empty ManySortedSign, z being 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,A9);
A11:  f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) by A1;
      for n being Nat, z being set st z = h.n holds
     h.(n+1) = o(z,n) from CIRCCMB2'sch_3(A11,A10);
then A12:  dom h = NAT & h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat holds h.(n+1) = F(n,h.n) by A2,PBOOLE:def 3;
   consider h1 being ManySortedSet of NAT such that
A13:  n-BitBorrowOutput(x,y) = h1.n and
A14:  h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat holds h1.(n+1) = BorrowOutput(x .(n+1), y.(n+1), h1.n)
         by Def3;
A15:  dom h1 = NAT & h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat holds h1.(n+1) = F(n,h1.n) by A14,PBOOLE:def 3;
      h = h1 from LambdaRecUn(A12,A15);
   hence thesis by A13;
  end;

theorem Th2:
  for a,b being 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;
  consider f,g,h being ManySortedSet of NAT such that
A1:   0-BitSubtracterStr(a,b) = f.0 & 0-BitSubtracterCirc(a,b) = g.0 and
A2:   f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
A3:   g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) and
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
    for n being Nat, S being non empty ManySortedSign,
          A being non-empty MSAlgebra over S
      for z being 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;
  thus 0-BitSubtracterStr(a,b)
      = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) by A1,A2;
  thus 0-BitSubtracterCirc(a,b)
      = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) by A1,A3;
       InnerVertices (0-BitSubtracterStr(a,b))
      = { [<*>,(0-tuples_on BOOLEAN)-->TRUE] } by A1,A2,CIRCCOMB:49;
   hence thesis by TARSKI:def 1;
  end;

theorem Th3:
for a,b being FinSequence, c being 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 being FinSequence, c be set such that
A1:  c = [<*>, (0-tuples_on BOOLEAN)-->TRUE];
   consider f,g,h being 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) &
    g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = c and
A5:  for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    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;
      c in the carrier of BitSubtracterWithBorrowStr(a.1, b.1, c) &
    1-BitBorrowOutput(a,b) = h.(0+1) by A1,A4,A5,Th1,FSCIRC_1:21;
   hence thesis by A2,A3,A4,A5;
  end;

theorem ::Col002a:
   for a,b,c being 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;
      <*a*>.1 = a & <*b*>.1 = b by FINSEQ_1:57;
   hence thesis by Th3;
  end;

theorem Th5:
 for n be Nat
 for p,q being FinSeqLen of n
 for p1,p2, q1,q2 being 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 F(Nat,set) = BorrowOutput((p^p1) .($1+1), (q^q1).($1+1), $2);
   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 being ManySortedSet of NAT such that
A1: n-BitSubtracterStr(p^p1,q^q1) = f1.n &
    n-BitSubtracterCirc(p^p1,q^q1) = g1.n and
A2: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h1.0 = c and
A3: for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    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 being ManySortedSet of NAT such that
A4: n-BitSubtracterStr(p^p2,q^q2) = f2.n &
    n-BitSubtracterCirc(p^p2,q^q2) = g2.n and
A5: f2.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g2.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h2.0 = c and
A6: for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    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;
A7:  L[0] by A2,A5;
A8:  for i being Nat st L[i] holds L[i+1]
     proof let i be Nat such that
A9:   i <= n implies h1.i = h2.i & f1.i = f2.i & g1.i = g2.i and
A10:   i+1 <= n;
        len p = n & len q = n by CIRCCOMB:def 12;
then A11:   dom p = Seg n & dom q = Seg n by FINSEQ_1:def 3;
        0 <= i by NAT_1:18;
      then 0+1 <= i+1 by AXIOMS:24;
      then i+1 in Seg n by A10,FINSEQ_1:3;
then A12:   (p^p1).(i+1) = p.(i+1) & (p^p2).(i+1) = p.(i+1) &
      (q^q1).(i+1) = q.(i+1) & (q^q2).(i+1) = q.(i+1) by A11,FINSEQ_1:def 7;
      defpred P[set,set,set,set] means not contradiction;
A13:   ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
         x being set st
       S = f1.0 & A = g1.0 & x = h1.0 & P [S,A,x,0] by A2;
A14:   for n being Nat, S being non empty ManySortedSign,
          A being non-empty MSAlgebra over S
      for x being 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];
A15:   for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
      for z being set, n being Nat holds
        A(S,A,z,n) is non-empty MSAlgebra over S(S,z,n);
        for n being Nat
      ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
       st S = f1.n & A = g1.n & P[S,A,h1.n,n]
         from CIRCCMB2'sch_13(A13,A3,A14,A15);
     then consider S being non empty ManySortedSign,
              A being non-empty MSAlgebra over S such that
A16:   S = f1.i & A = g1.i;
     thus h1.(i+1)
           = BorrowOutput((p^p2).(i+1), (q^q2).(i+1), h2.i) by A3,A9,A10,A12,
A16,NAT_1:38
          .= h2.(i+1) by A6,A9,A10,A16,NAT_1:38;
     thus f1.(i+1)
        = S+*BitSubtracterWithBorrowStr((p^p2).(i+1), (q^q2).(i+1), h2.i)
          by A3,A9,A10,A12,A16,NAT_1:38
       .= f2.(i+1) by A6,A9,A10,A16,NAT_1:38;
     thus g1.(i+1)
        = A+*BitSubtracterWithBorrowCirc((p^p2).(i+1), (q^q2).(i+1), h2.i)
          by A3,A9,A10,A12,A16,NAT_1:38
       .= g2.(i+1) by A6,A9,A10,A16,NAT_1:38;
    end;
A17:  for i being Nat holds L[i] from Ind(A7,A8);
   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,A4;
      n-BitBorrowOutput(p^p1, q^q1) = h1.n &
    n-BitBorrowOutput(p^p2, q^q2) = h2.n by A2,A3,A5,A6,Th1;
   hence thesis by A17;
  end;

theorem ::Col002b:
   for n be Nat for x,y being FinSeqLen of n for a,b being 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 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 being ManySortedSet of NAT such that
A1:  n-BitSubtracterStr(p,q) = f.n & n-BitSubtracterCirc(p,q) = g.n and
A2:  f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = c and
A3:  for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    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;
A4:  n-BitBorrowOutput(x^<*a*>, y^<*b*>) = h.n &
    (n+1)-BitSubtracterStr(x^<*a*>, y^<*b*>) = f.(n+1) &
    (n+1)-BitSubtracterCirc(x^<*a*>, y^<*b*>) = g.(n+1) &
    (n+1)-BitBorrowOutput(x^<*a*>, y^<*b*>) = h.(n+1) by A2,A3,Th1;
      len x = n & len y = n by CIRCCOMB:def 12;
then A5:  p.(n+1) = a & q.(n+1) = b by FINSEQ_1:59;
      x^<*> = x & y^<*> = y by FINSEQ_1:47;
    then n-BitSubtracterStr(p, q) = n-BitSubtracterStr(x, y) &
    n-BitSubtracterCirc(p, q) = n-BitSubtracterCirc(x, y) &
    n-BitBorrowOutput(p, q) = n-BitBorrowOutput(x, y) by Th5;
   hence thesis by A1,A3,A4,A5;
  end;

theorem Th7:
 for n be Nat for x,y being 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 being ManySortedSet of NAT such that
A1:  n-BitSubtracterStr(x,y) = f.n & n-BitSubtracterCirc(x,y) = g.n and
A2:  f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h.0 = c and
A3:  for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    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;
      n-BitBorrowOutput(x, y) = h.n &
    (n+1)-BitSubtracterStr(x, y) = f.(n+1) &
    (n+1)-BitSubtracterCirc(x, y) = g.(n+1) &
    (n+1)-BitBorrowOutput(x, y) = h.(n+1) by A2,A3,Th1;
   hence thesis by A1,A3;
  end;

::------------------------------------------------------------
:: Inner and Input-Vertex of n-Bit Full Subtracter Structure
::------------------------------------------------------------

theorem Th8:
 for n,m be Nat st n <= m
 for x,y being 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 being Nat such that
A2:  m = n+i by A1,NAT_1:28;
     defpred L[Nat] means
       InnerVertices (n-BitSubtracterStr(x,y)) c=
        InnerVertices ((n+$1)-BitSubtracterStr(x,y));
A3: L[0];
A4: for j being 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,XBOOLE_1:1;
        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;
        then InnerVertices (n-BitSubtracterStr(x,y)) c=
          InnerVertices (((n+j)+1)-BitSubtracterStr(x,y)) by Th7;
         hence thesis by XCMPLX_1:1;
     end;
   for j being Nat holds L[j] from Ind(A3,A4);
   hence thesis by A2;
  end;

theorem
   for n be Nat
 for x,y being 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 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 such that
A1:    k >= 1 & k <= n;
 let x,y be FinSequence;
 func (k,n)-BitSubtracterOutput(x,y) ->
      Element of InnerVertices (n-BitSubtracterStr(x,y)) means:Def4:
  ex i being Nat st k = i+1 &
   it = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y));
 uniqueness by XCMPLX_1:2;
 existence
  proof consider i being Nat such that
A2:  k = 1+i by A1,NAT_1:28;
   set o = BitSubtracterOutput(x .k, y.k, i-BitBorrowOutput(x,y));
A3:  InnerVertices (k-BitSubtracterStr(x,y)) c=
      InnerVertices (n-BitSubtracterStr(x,y)) by A1,Th8;
A4:  o in InnerVertices BitSubtracterWithBorrowStr(x .(i+1), y.(i+1),
           i-BitBorrowOutput(x, y)) by A2,FSCIRC_1:24;
A5:  k-BitSubtracterStr(x,y) = (i-BitSubtracterStr(x, y)) +*
     BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), i-BitBorrowOutput(x, y))
      by A2,Th7;
   reconsider o as Element of
    BitSubtracterWithBorrowStr(x .(i+1), y.(i+1), i-BitBorrowOutput(x, y))
     by A4;
      (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 A5,CIRCCOMB:def 2;
    then o in the carrier of k-BitSubtracterStr(x,y) by XBOOLE_0:def 2;
    then o in InnerVertices (k-BitSubtracterStr(x,y))
       by A4,A5,CIRCCOMB:19;
   hence thesis by A2,A3;
  end;
end;

theorem
   for n,k being Nat st k < n
 for x,y being FinSequence holds
  (k+1,n)-BitSubtracterOutput(x,y) =
     BitSubtracterOutput(x .(k+1), y.(k+1), k-BitBorrowOutput(x,y))
  proof let n,k be Nat such that
A1:  k < n;
   let x,y be FinSequence;
A2:  k+1 >= 1 by NAT_1:29;
      k+1 <= n by A1,NAT_1:38;
   then consider i being Nat such that
A3:  k+1 = i+1 & (k+1,n)-BitSubtracterOutput(x,y) =
     BitSubtracterOutput(x .(k+1), y.(k+1), i-BitBorrowOutput(x,y)) by A2,Def4;
   thus thesis by A3,XCMPLX_1:2;
  end;

theorem
   for n being Nat
 for x,y being FinSequence holds
  InnerVertices (n-BitSubtracterStr(x,y)) is Relation
  proof let n be 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 being Nat holds P[i] from Ind(A1,A2);
   hence thesis;
  end;

theorem Th12:
 for x,y,c being 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:55;
A2:   1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2)
          by CIRCCOMB:55;
       BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>,and2a) +*
         1GateCircStr(<*y,c*>,and2) +* 1GateCircStr(<*x,c*>,and2a)
         by FSCIRC_1:def 3;
     then InnerVertices BorrowIStr(x,y,c) =
          InnerVertices(1GateCircStr(<*x,y*>,and2a) +*
            1GateCircStr(<*y,c*>,and2)) \/
               InnerVertices(1GateCircStr(<*x,c*>,and2a)) by A1,CIRCCOMB:15
       .= InnerVertices(1GateCircStr(<*x,y*>,and2a)) \/
            InnerVertices(1GateCircStr(<*y,c*>,and2)) \/
            InnerVertices(1GateCircStr(<*x,c*>,and2a)) by A2,CIRCCOMB:15
       .= {[<*x,y*>,and2a]} \/
          InnerVertices(1GateCircStr(<*y,c*>,and2)) \/
          InnerVertices(1GateCircStr(<*x,c*>,and2a)) by CIRCCOMB:49
       .= {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/
          InnerVertices(1GateCircStr(<*x,c*>,and2a)) by CIRCCOMB:49
       .= {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]}
        by CIRCCOMB:49
       .= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]}
        by ENUMSET1:41
       .= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
        by ENUMSET1:43;
       hence thesis;
    end;

theorem Th13:
 for x,y,c being 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
A1:   x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] &
     c <> [<*x,y*>, and2a];
A2:   1GateCircStr(<*x,y*>,and2a) +* 1GateCircStr(<*y,c*>,and2) tolerates
       1GateCircStr(<*x,c*>,and2a)
          by CIRCCOMB:55;
A3:   1GateCircStr(<*x,y*>,and2a) tolerates 1GateCircStr(<*y,c*>,and2)
          by CIRCCOMB:55;
A4:  y in {1,y} & y in {2,y} by TARSKI:def 2;
       [1,y] = {{1,y},{1}} & [2,y] = {{2,y},{2}} by TARSKI:def 5;
then A5:  {1,y} in [1,y] & {2,y} in [2,y] by TARSKI:def 2;
      <*y,c*> = <*y*>^<*c*> by FINSEQ_1:def 9;
then A6: <*y*> c= <*y,c*> by FINSEQ_6:12;
       <*y*> = {[1,y]} by FINSEQ_1:def 5;
     then A7: [1,y] in <*y*> by TARSKI:def 1;
       [<*y,c*>,and2] = {{<*y,c*>,and2}, {<*y,c*>}} by TARSKI:def 5;
then A8:  <*y,c*> in {<*y,c*>} & {<*y,c*>} in [<*y,c*>,and2]
      by TARSKI:def 1,def 2;
then A9:  y <> [<*y,c*>,and2] by A4,A5,A6,A7,ORDINAL1:5;

A10:  c in {2,c} by TARSKI:def 2;
       [2,c] = {{2,c},{2}} by TARSKI:def 5;
then A11:  {2,c} in [2,c] by TARSKI:def 2;

       2 in dom <*y,c*> & <*y,c*>.2 = c
        proof
          dom <*y*> = Seg 1 by FINSEQ_1:def 8;
then A12:     len <*y*> = 1 by FINSEQ_1:def 3;
           dom <*c*> = Seg 1 by FINSEQ_1:def 8;
then A13:     len <*c*> = 1 by FINSEQ_1:def 3;
          dom<*y,c*> = dom(<*y*>^<*c*>) by FINSEQ_1:def 9
        .= Seg 2 by A12,A13,FINSEQ_1:def 7;
        hence thesis by FINSEQ_1:3,61;
       end;
     then [2,c] in <*y,c*> by FUNCT_1:8;
then A14:  c <> [<*y,c*>,and2] by A8,A10,A11,ORDINAL1:5;
       2 in dom <*x,y*> & <*x,y*>.2 = y
        proof
          dom <*x*> = Seg 1 by FINSEQ_1:def 8;
then A15:     len <*x*> = 1 by FINSEQ_1:def 3;
           dom <*y*> = Seg 1 by FINSEQ_1:def 8;
then A16:     len <*y*> = 1 by FINSEQ_1:def 3;
          dom<*x,y*> = dom(<*x*>^<*y*>) by FINSEQ_1:def 9
        .= Seg 2 by A15,A16,FINSEQ_1:def 7;
        hence thesis by FINSEQ_1:3,61;
       end;
then A17:  [2,y] in <*x,y*> by FUNCT_1:8;
       [<*x,y*>,and2a] = {{<*x,y*>,and2a}, {<*x,y*>}} by TARSKI:def 5;
     then <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,and2a]
      by TARSKI:def 1,def 2;
then y <> [<*x,y*>,and2a] by A4,A5,A17,ORDINAL1:5;
then A18:  not [<*x,y*>,and2a] in {y,c} by A1,TARSKI:def 2;
A19:  x in {1,x} by TARSKI:def 2;
       [1,x] = {{1,x},{1}} by TARSKI:def 5;
then A20:  {1,x} in [1,x] by TARSKI:def 2;
      <*x,y*> = <*x*>^<*y*> by FINSEQ_1:def 9;
then A21: <*x*> c= <*x,y*> by FINSEQ_6:12;
       <*x*> = {[1,x]} by FINSEQ_1:def 5;
     then A22: [1,x] in <*x*> by TARSKI:def 1;
       [<*x,y*>,and2a] = {{<*x,y*>,and2a}, {<*x,y*>}} by TARSKI:def 5;
     then <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,and2a]
      by TARSKI:def 1,def 2;
then x <> [<*x,y*>,and2a] by A19,A20,A21,A22,ORDINAL1:5;
then A23:  not c in {[<*x,y*>,and2a], [<*y,c*>,and2]} &
     not x in {[<*x,y*>,and2a], [<*y,c*>,and2]}
                          by A1,A14,TARSKI:def 2;
A24:  c in {2,c} by TARSKI:def 2;
       [2,c] = {{2,c},{2}} by TARSKI:def 5;
then A25:  {2,c} in [2,c] by TARSKI:def 2;
       2 in dom <*x,c*> & <*x,c*>.2 = c
        proof
           dom <*c*> = Seg 1 by FINSEQ_1:def 8;
then A26:     len <*c*> = 1 by FINSEQ_1:def 3;
           dom <*x*> = Seg 1 by FINSEQ_1:def 8;
then A27:     len <*x*> = 1 by FINSEQ_1:def 3;
          dom<*x,c*> = dom(<*x*>^<*c*>) by FINSEQ_1:def 9
        .= Seg 2 by A26,A27,FINSEQ_1:def 7;
        hence thesis by FINSEQ_1:3,61;
       end;
then A28:  [2,c] in <*x,c*> by FUNCT_1:8;
       [<*x,c*>,and2a] = {{<*x,c*>,and2a}, {<*x,c*>}} by TARSKI:def 5;
     then <*x,c*> in {<*x,c*>} & {<*x,c*>} in [<*x,c*>,and2a]
      by TARSKI:def 1,def 2;
then A29:  c <> [<*x,c*>,and2a] by A24,A25,A28,ORDINAL1:5;
A30:  x in {1,x} by TARSKI:def 2;
       [1,x] = {{1,x},{1}} by TARSKI:def 5;
then A31:  {1,x} in [1,x] by TARSKI:def 2;
      <*x,c*> = <*x*>^<*c*> by FINSEQ_1:def 9;
then A32: <*x*> c= <*x,c*> by FINSEQ_6:12;
      <*x*> = {[1,x]} by FINSEQ_1:def 5;
     then A33: [1,x] in <*x*> by TARSKI:def 1;
       [<*x,c*>,and2a] = {{<*x,c*>,and2a}, {<*x,c*>}} by TARSKI:def 5;
     then <*x,c*> in {<*x,c*>} & {<*x,c*>} in [<*x,c*>,and2a]
      by TARSKI:def 1,def 2;
then x <> [<*x,c*>,and2a] by A30,A31,A32,A33,ORDINAL1:5;
then A34:  not [<*x,c*>,and2a] in {x,y,c} by A1,A29,ENUMSET1:13;

       BorrowIStr(x,y,c) = 1GateCircStr(<*x,y*>,and2a) +*
         1GateCircStr(<*y,c*>,and2) +* 1GateCircStr(<*x,c*>,and2a)
         by FSCIRC_1:def 3;
     then 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 A2,CIRCCMB2:6

       .= ((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 A3,CIRCCMB2:6

       .= ((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 A3,CIRCCOMB:15

       .= ((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:49

       .= ((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:49

       .= ((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:49

       .= ((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:49

       .= ((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:49
       .= (({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:41
       .= (({x,y} \/ ({y,c} \ {[<*x,y*>,and2a]})) \
           {[<*x,c*>,and2a]}) \/
           ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A1,A9,FACIRC_2:1
       .= ({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]} \/
          ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A18,ZFMISC_1:65
       .= ({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]} \/ {x,c} by A23,ZFMISC_1:72
       .= {x,y,y,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:45
       .= {y,y,x,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:110
       .= {y,x,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:71
       .= {x,y,c} \ {[<*x,c*>,and2a]} \/ {x,c} by ENUMSET1:99
       .= {x,y,c} \/ {x,c} by A34,ZFMISC_1:65
       .= {x,y,c,c,x} by ENUMSET1:49
       .= {x,y,c,c} \/ {x} by ENUMSET1:50
       .= {c,c,x,y} \/ {x} by ENUMSET1:118
       .= {c,x,y} \/ {x} by ENUMSET1:71
       .= {c,x,y,x} by ENUMSET1:46
       .= {x,x,y,c} by ENUMSET1:113
       .= {x,y,c} by ENUMSET1:71;
       hence thesis;
  end;

theorem Th14:
 for x,y,c being 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:55;
A2:  Cyc tolerates (Cxc +* Cxyc) by CIRCCOMB:55;
A3:  Cxc tolerates Cxyc by CIRCCOMB:55;
A4:  InnerVertices (Cyc +* (Cxc +* Cxyc)) =
       InnerVertices Cyc \/ InnerVertices (Cxc +* Cxyc) by A2,CIRCCOMB:15;
A5:  InnerVertices (Cxc +* Cxyc) =
       InnerVertices Cxc \/ InnerVertices Cxyc by A3,CIRCCOMB:15;
   thus
      InnerVertices BorrowStr(x,y,c) =
      InnerVertices (BorrowIStr(x,y,c) +* Cxyc) by FSCIRC_1:def 4
     .= InnerVertices (Cxy +* Cyc +* Cxc +* Cxyc)
        by FSCIRC_1:def 3
     .= InnerVertices (Cxy +* (Cyc +* Cxc) +* Cxyc) by CIRCCOMB:10
     .= InnerVertices (Cxy +* (Cyc +* Cxc +* Cxyc)) by CIRCCOMB:10
     .= InnerVertices Cxy \/ InnerVertices (Cyc +* Cxc +* Cxyc)
          by A1,CIRCCOMB:15
     .= InnerVertices Cxy \/ InnerVertices (Cyc +* (Cxc +* Cxyc))
          by CIRCCOMB:10
     .= 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:49
     .= {xy} \/ {yc} \/ InnerVertices Cxc \/
          InnerVertices Cxyc by CIRCCOMB:49
     .= {xy} \/ {yc} \/ {xc} \/ InnerVertices Cxyc by CIRCCOMB:49
     .= {xy, yc} \/ {xc} \/ InnerVertices Cxyc by ENUMSET1:41
     .= {xy, yc, xc} \/ InnerVertices Cxyc by ENUMSET1:43
     .= {xy, yc, xc} \/
        {[<*[<*x,y*>, and2a], [<*y,c*>, and2], [<*x,c*>, and2a]*>, or3]}
        by CIRCCOMB:49
     .= {xy, yc, xc} \/ {BorrowOutput(x,y,c)} by FSCIRC_1:def 6;
  end;

theorem Th15:
 for x,y,c being 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:49;
A2:   InputVertices S = rng <*xy, yc, xc*> by CIRCCOMB:49
                    .= {xy, yc, xc} by FINSEQ_2:148;
    set BI = BorrowIStr(x,y,c);
    assume
A3:   x <> yc & y <> xc & c <> xy;
       rng <*x,c*> = {x,c} by FINSEQ_2:147;
     then A4: x in rng <*x,c*> by TARSKI:def 2;
       len <*xy, yc, xc*> = 3 by FINSEQ_1:62;
then A5:   Seg 3 = dom <*xy, yc, xc*> by FINSEQ_1:def 3;
then A6:  3 in dom <*xy, yc, xc*> by FINSEQ_1:3;
       <*xy, yc, xc*>.3 = xc by FINSEQ_1:62;
     then [3,xc] in <*xy, yc, xc*> by A6,FUNCT_1:8;
     then xc in rng <*xy, yc, xc*> by RELAT_1:def 5;
     then A7: the_rank_of xc in the_rank_of [<*xy, yc, xc*>, or3] by CIRCCOMB:
50;
       rng <*x,y*> = {x,y} by FINSEQ_2:147;
     then A8: y in rng <*x,y*> by TARSKI:def 2;
A9:  1 in dom <*xy, yc, xc*> by A5,FINSEQ_1:3;
       <*xy, yc, xc*>.1 = xy by FINSEQ_1:62;
     then [1,xy] in <*xy, yc, xc*> by A9,FUNCT_1:8;
     then xy in rng <*xy, yc, xc*> by RELAT_1:def 5;
     then A10: the_rank_of xy in the_rank_of [<*xy, yc, xc*>, or3] by CIRCCOMB:
50;
       rng <*y,c*> = {y,c} by FINSEQ_2:147;
     then A11: c in rng <*y,c*> by TARSKI:def 2;
A12:  2 in dom <*xy, yc, xc*> by A5,FINSEQ_1:3;
       <*xy, yc, xc*>.2 = yc by FINSEQ_1:62;
     then [2,yc] in <*xy, yc, xc*> by A12,FUNCT_1:8;
     then yc in rng <*xy, yc, xc*> by RELAT_1:def 5;
     then A13: the_rank_of yc in the_rank_of [<*xy, yc, xc*>, or3] by CIRCCOMB:
50;
A14:  {xy, yc, xc} \ {xy, yc, xc} = {} by XBOOLE_1:37;
A15:  {x, y, c} \ {[<*xy, yc, xc*>, or3]} = {x, y, c}
      proof
       thus {x,y,c} \ {[<*xy, yc, xc*>, or3]} c= {x,y,c} by XBOOLE_1:36;
       let a be set; assume
A16:     a in {x,y,c};
        then a = x or a = y or a = c by ENUMSET1:13;
        then a <> [<*xy, yc, xc*>, or3] by A4,A7,A8,A10,A11,A13,CIRCCOMB:50;
        then not a in {[<*xy, yc, xc*>, or3]} by TARSKI:def 1;
       hence thesis by A16,XBOOLE_0:def 4;
      end;
        BorrowStr(x,y,c) = BI+*S & BI tolerates S
       by CIRCCOMB:55,FSCIRC_1:def 4;
   hence InputVertices BorrowStr(x,y,c)
     = ((InputVertices BI) \ InnerVertices S) \/
       ((InputVertices S) \ InnerVertices BI) by CIRCCMB2:6
    .= {x,y,c} \/ ({xy, yc, xc} \ InnerVertices BI)
        by A1,A2,A3,A15,Th13
    .= {x,y,c} \/ {} by A14,Th12
    .= {x,y,c};
  end;

theorem Th16:
 for x,y,c being 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] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] and
A2: c <> [<*x,y*>, 'xor'];
A3: BitSubtracterWithBorrowStr(x,y,c)
      = 2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c) by FSCIRC_1:def 8;
A4: InputVertices 2GatesCircStr(x,y,c, 'xor') = {x,y,c} by A2,FACIRC_1:57;
A5: InputVertices BorrowStr(x,y,c) = {x,y,c} by A1,Th15;
      2GatesCircStr(x,y,c, 'xor') tolerates BorrowStr(x,y,c) by CIRCCOMB:55;
   hence thesis by A3,A4,A5,FACIRC_2:22;
 end;

theorem Th17:
 for x,y,c being 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;
A1:   2GatesCircStr(x,y,c, 'xor') tolerates BorrowStr(x,y,c) by CIRCCOMB:55;
       InnerVertices BitSubtracterWithBorrowStr(x,y,c) =
     InnerVertices (2GatesCircStr(x,y,c, 'xor') +* BorrowStr(x,y,c))
       by FSCIRC_1:def 8
  .= InnerVertices 2GatesCircStr(x,y,c, 'xor') \/
       InnerVertices BorrowStr(x,y,c) by A1,CIRCCOMB:15
  .= {[<*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;

definition
 let n be Nat;
 let x,y be FinSequence;
 cluster n-BitBorrowOutput(x,y) -> pair;
 coherence
  proof
   consider h being ManySortedSet of NAT such that
A1: 0-BitBorrowOutput(x,y) = h.0 and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] and
      for n being 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;
A3:  P[0] by A1,A2;
A4:  for n being 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]
         by FSCIRC_1:def 6;
      hence thesis;
     end;
      for n being Nat holds P[n] from Ind(A3,A4);
   hence thesis;
  end;
end;

theorem Th18:
 for x,y being FinSequence, n being 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;
      [<*>, (0-tuples_on BOOLEAN)-->TRUE]`2 = (0-tuples_on BOOLEAN)-->TRUE &
    dom ((0-tuples_on BOOLEAN)-->TRUE) = 0-tuples_on BOOLEAN &
    0-BitBorrowOutput(x,y) = [<*>, (0-tuples_on BOOLEAN)-->TRUE]
     by Th2,FUNCOP_1:19,MCART_1:7;
then A1: P[0] by FUNCT_5:21,MCART_1:7;
A2: now let n be Nat; assume P[n];
     set c = n-BitBorrowOutput(x, y);
        (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] by FSCIRC_1:def 6;
      then dom or3 = 3-tuples_on BOOLEAN & ((n+1)-BitBorrowOutput(x, y))`1 =
        <*[<*x .(n+1),y.(n+1)*>, and2a], [<*y.(n+1),c*>, and2],
          [<*x .(n+1),c*>, and2a]*> &
      ((n+1)-BitBorrowOutput(x, y))`2 = or3 by FUNCT_2:def 1,MCART_1:7;
      hence P[n+1] by FINSEQ_1:62,FUNCT_5:21;
    end;
   thus for i being Nat holds P[i] from Ind(A1,A2);
  end;

theorem Th19:
 for n being Nat, x,y being FinSequence, p being 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;
     dom and2 = 2-tuples_on BOOLEAN &
   dom and2a = 2-tuples_on BOOLEAN & dom 'xor' = 2-tuples_on BOOLEAN &
    [p, and2]`2 = and2 & [p, and2a]`2 = and2a & [p, 'xor']`2 = 'xor'
      by FUNCT_2:def 1,MCART_1:7;
then A1: proj1 [p, and2]`2 = 2-tuples_on BOOLEAN &
    proj1 [p, and2a]`2 = 2-tuples_on BOOLEAN &
    proj1 [p, 'xor']`2 = 2-tuples_on BOOLEAN by FUNCT_5:21;
      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 A1,PRALG_1:1;
  end;

::-----------------------------------------------------
:: Relation and Pair for n-Bit Full Subtracter
::-----------------------------------------------------

theorem Th20:
 for f,g being nonpair-yielding FinSequence
 for n being 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 being ManySortedSet of NAT such that
A1:  for n being Nat holds h.n = F(n) from LambdaDMS;
   deffunc h(Nat) = h.$1;
   deffunc o(set, Nat) = BorrowOutput(f.($2+1),g.($2+1), $1);
   set k = (0-tuples_on BOOLEAN)-->TRUE;
A2: 0-BitSubtracterStr(f,g) = 1GateCircStr(<*>, k) by Th2;
then A3:  InnerVertices Sn(0) is Relation by FACIRC_1:38;
A4:  InputVertices Sn(0) is without_pairs by A2,FACIRC_1:39;
      h(0) = 0-BitBorrowOutput(f,g) by A1;
then A5:  h.0 in InnerVertices Sn(0);
A6:  for n being Nat, x being set holds InnerVertices S(x,n) is Relation
     by FSCIRC_1:22;
A7: now let n be Nat, x be set such that
A8:    x = h(n);
A9:    h(n) = n-BitBorrowOutput(f,g) by A1;
A10:    f.(n+1) <> [<*g.(n+1),x*>, and2] & g.(n+1) <> [<*f.(n+1),x*>, and2a];
         x <> [<*f.(n+1),g.(n+1)*>, and2a] & x <> [<*f.(n+1),g.(n+1)*>, 'xor']
        by A8,A9,Th19;
      hence InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A10,Th16;
    end;
A11:  for n being Nat, x being set st x = h.n holds
       (InputVertices S(x, n)) \ {x} is without_pairs
     proof let n be Nat, x be set such that
A12:    x = h(n);
A13:    InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A7,A12;
      thus (InputVertices S(x, n)) \ {x} is without_pairs
       proof let a be pair set; assume a in (InputVertices S(x, n)) \ {x};
         then a in InputVertices S(x, n) & not a in {x} by XBOOLE_0:def 4;
         then (a = f.(n+1) or a = g.(n+1) or a = x) & not a in {x}
            by A13,ENUMSET1:13;
        hence contradiction by TARSKI:def 1;
       end;
     end;
A14:  now let n be Nat, S be non empty ManySortedSign, x be set; assume
A15:   S = Sn(n) & x = h.n;
then A16:   x = n-BitBorrowOutput(f,g) & h(n+1) = (n+1)-BitBorrowOutput(f,g)
       by A1;
     hence Sn(n+1) = S +* S(x,n) by A15,Th7;
     thus h.(n+1) = o(x, n) by A16,Th7;
        InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A7,A15;
     hence x in InputVertices S(x,n) by ENUMSET1:14;
A17:   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 A17,XBOOLE_0:def 2;
    end;
A18:  for n being Nat holds
     InputVertices Sn(n+1) =
      (InputVertices Sn(n))\/((InputVertices S(h.(n),n)) \ {h.(n)}) &
     InnerVertices Sn(n) is Relation &
     InputVertices Sn(n) is without_pairs from CIRCCMB2'sch_11(A3,A4,A5,A6,A11,
A14);
   let n be Nat; h.n = n-BitBorrowOutput(f,g) by A1;
   hence thesis by A18;
  end;

theorem
   for n being Nat
 for x,y being nonpair-yielding FinSeqLen of n holds
  InputVertices (n-BitSubtracterStr(x,y)) = rng x \/ rng y
  proof defpred P[Nat] means
    for x,y being 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;
         len x = 0 & len y = 0 by CIRCCOMB:def 12;
then A2:    rng x = {} & rng y = {} by FINSEQ_1:25,RELAT_1:60;
       0-BitSubtracterStr(x,y) = 1GateCircStr(<*>, f) by Th2;
      hence InputVertices (0-BitSubtracterStr(x,y))
         = rng <*> by CIRCCOMB:49
        .= rng x \/ rng y by A2;
     end;
A3:  for i being Nat st P[i] holds P[i+1]
     proof let i be Nat such that
A4:    P[i];
      let x,y be nonpair-yielding FinSeqLen of i+1;
      consider x' being nonpair-yielding FinSeqLen of i,
               z1 being non pair set such that
A5:    x = x'^<*z1*> by FACIRC_2:36;
      consider y' being nonpair-yielding FinSeqLen of i,
               z2 being non pair set such that
A6:    y = y'^<*z2*> by FACIRC_2:36;
      set S = (i+1)-BitSubtracterStr(x, y);
A7:    1 in Seg 1 by FINSEQ_1:3;
then A8:    1 in dom <*z1*> by FINSEQ_1:def 8;
     len x' = i by CIRCCOMB:def 12;
then A9:    x .(i+1) = <*z1*>.1 by A5,A8,FINSEQ_1:def 7 .= z1 by FINSEQ_1:def 8
;
A10:    1 in dom <*z2*> by A7,FINSEQ_1:def 8;
     len y' = i by CIRCCOMB:def 12;
then A11:   y .(i+1) = <*z2*>.1 by A6,A10,FINSEQ_1:def 7 .= z2 by FINSEQ_1:def
8;
A12:    {z1,z2,i-BitBorrowOutput(x,y)} = {i-BitBorrowOutput(x,y),z1,z2}
         by ENUMSET1:100;
A13:    rng x = rng x' \/ rng <*z1*> by A5,FINSEQ_1:44
       .= rng x' \/ {z1} by FINSEQ_1:55;
A14:   rng y = rng y' \/ rng <*z2*> by A6,FINSEQ_1:44
       .= rng y' \/ {z2} by FINSEQ_1:55;
A15:    z1 <> [<*z2,i-BitBorrowOutput(x,y)*>, and2] &
       z2 <> [<*z1,i-BitBorrowOutput(x,y)*>, and2a] &
       i-BitBorrowOutput(x,y) <> [<*z1,z2*>, and2a] &
       i-BitBorrowOutput(x,y) <> [<*z1,z2*>, 'xor']
        by Th19;
         x' = x'^{} & y' = y'^{} by FINSEQ_1:47;
       then i-BitSubtracterStr(x,y) = i-BitSubtracterStr(x',y') by A5,A6,Th5;
      hence InputVertices S =
        (InputVertices (i-BitSubtracterStr(x',y')))\/
        ((InputVertices BitSubtracterWithBorrowStr(z1,z2,
          i-BitBorrowOutput(x,y)) \ {i-BitBorrowOutput(x,y)})) by A9,A11,Th20
       .= (rng x' \/ rng y')\/
        ((InputVertices BitSubtracterWithBorrowStr(z1,z2,
          i-BitBorrowOutput(x,y)) \ {i-BitBorrowOutput(x,y)})) by A4
       .= (rng x' \/ rng y')\/
        ({z1,z2,i-BitBorrowOutput(x,y)} \ {i-BitBorrowOutput(x,y)})
          by A15,Th16
       .= (rng x' \/ rng y')\/ {z1,z2} by A12,AMI_7:1
       .= rng x' \/ rng y' \/ ({z1} \/ {z2}) by ENUMSET1:41
       .= rng x' \/ rng y' \/ {z1} \/ {z2} by XBOOLE_1:4
       .= rng x' \/ {z1} \/ rng y' \/ {z2} by XBOOLE_1:4
       .= rng x \/ rng y by A13,A14,XBOOLE_1:4;
     end;
   thus for i being Nat holds P[i] from Ind(A1,A3);
  end;

::-----------------------------------------------------
:: Following theorem for n-Bit Full Subtracter Circuit
::-----------------------------------------------------

Lm1:
 for x,y,c being set
 for s being State of BorrowCirc(x,y,c)
  for a1,a2,a3 being 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 & a2 = s.y & a3 = s.c;
   set S = BorrowStr(x,y,c);
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
A4:  x in the carrier of S & y in the carrier of S & 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 A2,FACIRC_1:35
     .= and2a.<*a1,a2*> by A1,A3,A4,FINSEQ_2:145
     .= '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 A2,FACIRC_1:35
     .= and2.<*a2,a3*> by A1,A3,A4,FINSEQ_2:145
     .= a2 '&' a3 by TWOSCOMP:def 1;
      [<*x,c*>,and2a] in InnerVertices BorrowStr(x,y,c) by FSCIRC_1:7;
   hence (Following s).[<*x,c*>,and2a]
      = and2a.(s*<*x,c*>) by A2,FACIRC_1:35
     .= and2a.<*a1,a3*> by A1,A3,A4,FINSEQ_2:145
     .= 'not' a1 '&' a3 by TWOSCOMP:def 2;
  end;

theorem Th22:
 for x,y,c being set
 for s being State of BorrowCirc(x,y,c)
  for a1,a2,a3 being 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] & a2 = s.[<*y,c*>,and2] & a3 = s.[<*x,c*>,and2a];
   set x_y =[<*x,y*>,and2a], y_c = [<*y,c*>,and2], c_x = [<*x,c*>,and2a];
   set S = BorrowStr(x,y,c);
A2:  InnerVertices S = the OperSymbols of S by FACIRC_1:37;
A3:  dom s = the carrier of S by CIRCUIT1:4;
   reconsider x_y, y_c, c_x as Element of InnerVertices S by FSCIRC_1:7;
      BorrowOutput(x,y,c) = [<*x_y, y_c, c_x*>, or3] by FSCIRC_1:def 6;
   hence (Following s).BorrowOutput(x,y,c)
      = or3.(s*<*x_y, y_c, c_x*>) by A2,FACIRC_1:35
     .= or3.<*a1,a2,a3*> by A1,A3,FINSEQ_2:146
     .= a1 'or' a2 'or' a3 by FACIRC_1:def 7;
  end;

Lm2:
 for x,y,c being set st
   x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a]
  for s being State of BorrowCirc(x,y,c)
  for a1,a2,a3 being 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] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a];
   let s be State of BorrowCirc(x,y,c);
   let a1,a2,a3 be Element of BOOLEAN such that
A2:  a1 = s.x & a2 = s.y & a3 = s.c;
   set x_y =[<*x,y*>,and2a], y_c = [<*y,c*>,and2], c_x = [<*x,c*>,and2a];
   set S = BorrowStr(x,y,c);
   reconsider x' = x, y' = y, c' = c as Vertex of S by FSCIRC_1:6;
      InputVertices S = {x,y,c} by A1,Th15;
    then x in InputVertices S & y in InputVertices S & c in InputVertices S
     by ENUMSET1:14;
then A3:  (Following s).x' = s.x & (Following s).y' = s.y & (Following s).c' =
s.c
     by CIRCUIT2:def 5;
A4:  Following(s,2) = Following Following s by FACIRC_1:15;
    (Following s).x_y = 'not' a1 '&' a2 & (Following s).y_c = a2 '&' a3 &
    (Following s).c_x = 'not' a1 '&' a3 by A2,Lm1;
   hence (Following(s,2)).BorrowOutput(x,y,c) =
         'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 by A4,Th22;
   thus thesis by A2,A3,A4,Lm1;
  end;

theorem Th23:
 for x,y,c being set st
   x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
   c <> [<*x,y*>, 'xor']
 for s being 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
A1: x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
    c <> [<*x,y*>, 'xor'];
   let s be State of BorrowCirc(x,y,c);
A2:  dom Following Following(s,2) = the carrier of S &
    dom Following(s,2) = the carrier of S by CIRCUIT1:4;
   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;
      a1 = s.x & a2 = s.y & a3 = s.c;
then A3:  ffs.BorrowOutput(x,y,c)
       = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 &
    ffs.[<*x,y*>,and2a] = 'not' a1 '&' a2 &
    ffs.[<*y,c*>,and2] = a2 '&' a3 &
    ffs.[<*x,c*>,and2a] = 'not' a1 '&' a3 by A1,Lm2;
A4:  ffs = Following Following s by FACIRC_1:15;
       InputVertices S = {x,y,c} by A1,Th15;
then A5:  x in InputVertices S & y in InputVertices S & c in InputVertices S
       by ENUMSET1:14;
    then (Following s).x = a1 & (Following s).y = a2 & (Following s).c = a3
     by CIRCUIT2:def 5;
  then A6: ffs.x = a1 & ffs.y = a2 & ffs.c = a3 by A4,A5,CIRCUIT2:def 5;
      now let a be set; assume
A7:   a in the carrier of S;
     then reconsider v = a as Vertex of S;
A8:    v in InputVertices S \/ InnerVertices S by A7,MSAFREE2:3;
     thus ffs.a = (fffs).a
      proof per cases by A8,XBOOLE_0:def 2;
       suppose v in InputVertices S;
        hence thesis by CIRCUIT2:def 5;
       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 2;
         then v = [<*x,y*>,and2a] or v = [<*y,c*>,and2] or v = [<*x,c*>,and2a]
or
         v = BorrowOutput(x,y,c) by ENUMSET1:13,TARSKI:def 1;
        hence thesis by A3,A6,Lm1,Th22;
      end;
    end;
   hence ffs = fffs by A2,FUNCT_1:9;
  end;

theorem
   for x,y,c being set st
   x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
   c <> [<*x,y*>, 'xor']
 for s being State of BitSubtracterWithBorrowCirc(x,y,c)
 for a1,a2,a3 being 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] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
    c <> [<*x,y*>, 'xor'];
   set f = '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;
   let a1,a2,a3 be Element of BOOLEAN; assume
A2:  a1 = s.x & a2 = s.y & a3 = s.c;
A3: x in the carrier of S1 & y in the carrier of S1 & c in the carrier of S1
     by FACIRC_1:60;
A4: x in the carrier of S2 & y in the carrier of S2 & c in the carrier of S2
     by FSCIRC_1:6;
A5:  A = A1 +* A2 & S = S1+*S2 by FSCIRC_1:def 8,def 9;
   then 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 A5,FACIRC_1:26;
   reconsider t = s as State of A1+*A2 by A5;
A6: InputVertices S2 = {x,y,c} by A1,Th15;
  InnerVertices S1 misses InputVertices S1 &
    InnerVertices S2 misses InputVertices S2 by MSAFREE2:4;
then A7: InnerVertices S1 misses InputVertices S2 &
    InnerVertices S2 misses InputVertices S1 by A1,A6,FACIRC_1:57;
A8: BitSubtracterOutput(x,y,c) = 2GatesCircOutput(x,y,c, f) &
    BitSubtracterCirc(x,y,c) = 2GatesCircuit(x,y,c, f)
      by FSCIRC_1:def 1,def 2;
      dom s1 = the carrier of S1 by CIRCUIT1:4;
then a1 = s1.x & a2 = s1.y & a3 = s1.c by A2,A3,FUNCT_1:70;
    then (Following(t,2)).2GatesCircOutput(x,y,c, f)
      = (Following(s1,2)).2GatesCircOutput(x,y,c, f) &
    (Following(s1,2)).2GatesCircOutput(x,y,c,f) = a1 'xor' a2 'xor' a3
     by A1,A7,A8,FACIRC_1:32,64;
   hence (Following(s,2)).BitSubtracterOutput(x,y,c) = a1 'xor' a2 'xor' a3
      by A5,FSCIRC_1:def 1;
      dom s2 = the carrier of S2 by CIRCUIT1:4;
  then a1 = s2.x & a2 = s2.y & a3 = s2.c by A2,A4,FUNCT_1:70;
    then (Following(t,2)).BorrowOutput(x,y,c)
      = (Following(s2,2)).BorrowOutput(x,y,c) &
    (Following(s2,2)).BorrowOutput(x,y,c)
      = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3
          by A1,A7,Lm2,FACIRC_1:33;
   hence (Following(s,2)).BorrowOutput(x,y,c)
           = 'not' a1 '&' a2 'or' a2 '&' a3 'or' 'not' a1 '&' a3 by A5;
  end;

theorem Th25:
 for x,y,c being set st
   x <> [<*y,c*>, and2] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
   c <> [<*x,y*>, 'xor']
 for s being 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] & y <> [<*x,c*>, and2a] & c <> [<*x,y*>, and2a] &
    c <> [<*x,y*>, 'xor'];
   set f = '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;
A2:  A = A1 +* A2 & S = S1+*S2 by FSCIRC_1:def 8,def 9;
   then 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 A2,FACIRC_1:26;
   reconsider t = s as State of A1+*A2 by A2;
A3: InputVertices S2 = {x,y,c} by A1,Th15;
  InnerVertices S1 misses InputVertices S1 &
    InnerVertices S2 misses InputVertices S2 by MSAFREE2:4;
    then InnerVertices S1 misses InputVertices S2 &
    InnerVertices S2 misses InputVertices S1 by A1,A3,FACIRC_1:57;
then A4:  Following(s1,2) = Following(t,2)|the carrier of S1 &
    Following(s1,3) = Following(t,3)|the carrier of S1 &
    Following(s2,2) = Following(t,2)|the carrier of S2 &
    Following(s2,3) = Following(t,3)|the carrier of S2
      by FACIRC_1:30,31;
      A1 = 2GatesCircuit(x,y,c, f) by FSCIRC_1:def 2;
    then Following(s1,2) is stable by A1,FACIRC_1:63;
then A5: Following(s1,2) = Following Following(s1,2) by CIRCUIT2:def 6
                   .= Following(s1,2+1) by FACIRC_1:12;
      Following(s2,2) is stable by A1,Th23;
then A6: Following(s2,2) = Following Following(s2,2) by CIRCUIT2:def 6
                   .= Following(s2,2+1) by FACIRC_1:12;
A7: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
A8: dom Following(s,2) = the carrier of S &
    dom Following(s,3) = the carrier of S &
    dom Following(s1,2) = the carrier of S1 &
    dom Following(s2,2) = the carrier of S2 by CIRCUIT1:4;
      S = S1+*S2 by FSCIRC_1:def 8;
then A9:  the carrier of S = (the carrier of S1) \/ the carrier of S2
     by CIRCCOMB:def 2;
      now let a be set; assume a in the carrier of S;
      then a in the carrier of S1 or a in the carrier of S2 by A9,XBOOLE_0:def
2;
      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 A2,A4,A5,A6,A8,FUNCT_1:70;
     hence (Following(s,2)).a = (Following Following(s,2)).a
      by A5,A6,FACIRC_1:12;
    end;
   hence Following(s,2) = Following Following(s,2) by A7,A8,FUNCT_1:9;
  end;

theorem
   for n being Nat
 for x,y being nonpair-yielding FinSeqLen of n
 for s being State of n-BitSubtracterCirc(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) = 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);
   consider N being Function of NAT,NAT such that
A1: N.0 = 1 & N.1 = 2 & N.2 = n by FACIRC_2:37;
    deffunc n(Nat) = N.$1;
A2: for x being set, n being Nat holds
      A(x,n) is Boolean gate`2=den strict Circuit of S(x,n);
A3: 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(Nat) = $1-BitBorrowOutput(f,g);
   consider h being ManySortedSet of NAT such that
A4:  for n being Nat holds h.n = F(n) from LambdaDMS;
A5: for n being Nat, x being set
    for A being non-empty Circuit of S(x,n) st x = h.(n) & A = A(x,n)
    for s being State of A holds Following(s, n(1)) is stable
     proof let n be Nat, x be set, A be non-empty Circuit of S(x,n);
      assume x = h.n;
       then x = n-BitBorrowOutput(f,g) by A4;
       then f.(n+1) <> [<*g.(n+1),x*>, and2] & g.(n+1) <> [<*f.(n+1),x*>,
and2a] &
       x <> [<*f.(n+1),g.(n+1)*>, and2a] & x <> [<*f.(n+1),g.(n+1)*>, 'xor']
        by Th19;
      hence thesis by A1,Th25;
     end;
   set Sn = n-BitSubtracterStr(f,g);
   set An = n-BitSubtracterCirc(f,g);
   set o0 = 0-BitBorrowOutput(f,g);
   consider f1,g1,h1 being ManySortedSet of NAT such that
A6: n-BitSubtracterStr(f,g) = f1.n & n-BitSubtracterCirc(f,g) = g1.n and
A7: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->TRUE) &
    h1.0 = [<*>, (0-tuples_on BOOLEAN)-->TRUE] &
    for n being Nat, S being non empty ManySortedSign,
        A being non-empty MSAlgebra over S
    for z being 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 set; assume i in NAT;
     then reconsider j = i as Nat;
     thus h1.i = j-BitBorrowOutput(f,g) by A7,Th1 .= h.i by A4;
    end;
then A8: h1 = h by PBOOLE:3;
A9: ex u,v being ManySortedSet of NAT st
     Sn = u.(n(2)) & An = v.(n(2)) &
     u.0 = S0 & v.0 = A0 & h.0 = o0 &
     for n being Nat, S being non empty ManySortedSign,
         A1 being non-empty MSAlgebra over S
     for x being set, A2 being 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 A1,A4,A6,A7,A8;
     end;
A10: InnerVertices S0 is Relation & InputVertices S0 is without_pairs
     by FACIRC_1:38,39;
      [<*>, (0-tuples_on BOOLEAN)-->TRUE] = o0 &
    InnerVertices S0 = {[<*>, (0-tuples_on BOOLEAN)-->TRUE]}
     by Th2,CIRCCOMB:49;
then A11: h.0 = o0 & o0 in InnerVertices S0 by A4,TARSKI:def 1;
A12: for n being Nat, x being set holds InnerVertices S(x,n) is Relation
     by FSCIRC_1:22;
A13: for n being Nat, x being set st x = h.n holds
       (InputVertices S(x, n)) \ {x} is without_pairs
     proof let n be Nat, x be set such that
A14:    x = h.n;
         x = n-BitBorrowOutput(f,g) by A4,A14;
       then f.(n+1) <> [<*g.(n+1),x*>, and2] & g.(n+1) <> [<*f.(n+1),x*>,
and2a] &
       x <> [<*f.(n+1),g.(n+1)*>, and2a] & x <> [<*f.(n+1),g.(n+1)*>, 'xor']
        by Th19;
then A15:    InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by Th16;
      let a be pair set; assume a in (InputVertices S(x, n)) \ {x};
       then a in {f.(n+1),g.(n+1),x} & not a in {x} by A15,XBOOLE_0:def 4;
       then (a = f.(n+1) or a = g.(n+1) or a = x) & a <> x
        by ENUMSET1:13,TARSKI:def 1;
      hence thesis;
     end;
A16: for n being Nat, x being 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
A17:    x = h.n;
A18:    x = n-BitBorrowOutput(f,g) &
       h.(n+1) = (n+1)-BitBorrowOutput(f,g) by A4,A17;
      hence h.(n+1) = o(x, n) by Th7;
         f.(n+1) <> [<*g.(n+1),x*>, and2] & g.(n+1) <> [<*f.(n+1),x*>, and2a] &
       x <> [<*f.(n+1),g.(n+1)*>, and2a] & x <> [<*f.(n+1),g.(n+1)*>, 'xor']
        by A18,Th19;
      then InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by Th16;
      hence x in InputVertices S(x, n) by ENUMSET1:14;
      set xx = f.(n+1), xy = g.(n+1);
A19:    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 A19,XBOOLE_0:def 2;
     end;
      for s being State of n-BitSubtracterCirc(f,g) holds
     Following(s,n(0)+n(2)*n(1)) is stable
      from CIRCCMB2'sch_22(A2,A3,A5,A9,A10,A11,A12,A13,A16);
   hence thesis by A1;
  end;

Back to top