:: Full Adder Circuit. Part { II }
::  by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Katsumi Wasaki
::
:: Received March 22, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, RELAT_1, CLASSES1, STRUCT_0,
      CIRCCOMB, MSUALG_1, FUNCT_1, LATTICES, FUNCOP_1, MARGREL1, PARTFUN1,
      FUNCT_4, TARSKI, CARD_1, NAT_1, FINSEQ_2, XBOOLEAN, PBOOLE, ARYTM_3,
      FACIRC_1, SUBSET_1, CIRCUIT1, MSAFREE2, ORDINAL4, XXREAL_0, MCART_1,
      FSM_1, CIRCUIT2, GLIB_000, FACIRC_2;
 notations TARSKI, XBOOLE_0, ENUMSET1,
      XTUPLE_0, SUBSET_1, CARD_1, NUMBERS, ORDINAL1,
      NAT_1, MCART_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FUNCOP_1, FUNCT_4, PBOOLE, MARGREL1, BINARITH, CLASSES1, PARTFUN1,
      MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, XXREAL_0;
 constructors ENUMSET1, XXREAL_0, CLASSES1, BINARITH, CIRCUIT1, CIRCUIT2,
      FACIRC_1, NAT_1, RELSET_1, BINOP_1, WELLORD1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0,
      XREAL_0, NAT_1, FINSEQ_1, MARGREL1, FINSEQ_2, CARD_3, STRUCT_0, MSUALG_1,
      CIRCCOMB, FACIRC_1, CIRCCMB2, CARD_1, RELSET_1, MSAFREE2, FINSET_1,
      FUNCT_4, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions STRUCT_0, TARSKI, CIRCUIT2, CIRCCOMB, FACIRC_1, XBOOLE_0,
      MSAFREE2, MARGREL1, XTUPLE_0;
 theorems TARSKI, ZFMISC_1, ENUMSET1, MCART_1, NAT_1, ORDINAL1,
      FUNCT_1, FUNCT_2, FINSEQ_1, PARTFUN1, FUNCT_4, FINSEQ_6, PBOOLE,
      CIRCUIT2, CIRCCOMB, FACIRC_1, CIRCCMB2, CIRCUIT1, FUNCOP_1, XBOOLE_0,
      XBOOLE_1, FINSEQ_2, XREAL_1, CLASSES1, CARD_1, XTUPLE_0, XREGULAR;
 schemes NAT_1, CIRCCMB2, PBOOLE, PARTFUN1;

begin

theorem Th1:
  for x,y,z being set st x <> z & y <> z holds {x,y} \ {z} = {x,y}
proof
  let x,y,z be set;
  assume that
A1: x <> z and
A2: y <> z;
  for a being set st a in {x,y} holds not a in {z}
  proof
    let a be set;
    assume a in {x,y};
    then a <> z by A1,A2,TARSKI:def 2;
    hence thesis by TARSKI:def 1;
  end;
  then {x,y} misses {z} by XBOOLE_0:3;
  hence thesis by XBOOLE_1:83;
end;

theorem
  for x,y,z being set holds x <> [<*x,y*>, z] & y <> [<*x,y*>, z]
proof
  let x,y,z be set;
A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;
  then
A2: x in rng <*x,y*> by TARSKI:def 2;
A3: y in rng <*x,y*> by A1,TARSKI:def 2;
A4: the_rank_of x in the_rank_of [<*x,y*>,z] by A2,CLASSES1:82;
  the_rank_of y in the_rank_of [<*x,y*>,z] by A3,CLASSES1:82;
  hence thesis by A4;
end;

registration
  cluster void -> unsplit gate`1=arity gate`2isBoolean for ManySortedSign;
  coherence
  proof
    let S be ManySortedSign;
    assume
A1: the carrier' of S is empty;
    hence the ResultSort of S = {} .= id the carrier' of S by A1;
    thus S is gate`1=arity
    proof
      let g be set;
      thus thesis by A1;
    end;
    let g be set;
    thus thesis by A1;
  end;
end;

registration
  cluster strict void for ManySortedSign;
  existence
  proof set S = the strict void ManySortedSign;
    take S;
    thus thesis;
  end;
end;

definition
  let x be set;
  func SingleMSS(x) -> strict void ManySortedSign means
  :Def1:
  the carrier of it = {x};
  existence
  proof set a = the Function of {},{x}*;
    set r = the Function of {},{x};
    reconsider S = ManySortedSign(#{x}, {}, a, r#) as
    void strict ManySortedSign;
    take S;
    thus thesis;
  end;
  uniqueness
  proof
    let S1, S2 be strict void ManySortedSign such that
A1: the carrier of S1 = {x} and
A2: the carrier of S2 = {x};
    the Arity of S1 = the Arity of S2;
    hence thesis by A1,A2;
  end;
end;

registration
  let x be set;
  cluster SingleMSS(x) -> non empty;
  coherence
  proof
    the carrier of SingleMSS(x) = {x} by Def1;
    hence the carrier of SingleMSS(x) is non empty;
  end;
end;

definition
  let x be set;
  func SingleMSA(x) -> Boolean strict MSAlgebra over SingleMSS(x) means
  not contradiction;
  existence;
  uniqueness
  proof
    set S = SingleMSS(x);
    let A1, A2 be Boolean strict MSAlgebra over S;
A1: the Sorts of A1 = (the carrier of S) --> BOOLEAN by CIRCCOMB:57;
A2: the Charact of A1 = {};
    the Charact of A2 = {};
    hence thesis by A1,A2,CIRCCOMB:57;
  end;
end;

theorem
  for x being set, S being ManySortedSign holds SingleMSS x tolerates S
proof
  let x be set, S be ManySortedSign;
  thus the Arity of SingleMSS x tolerates the Arity of S &
  the ResultSort of SingleMSS x tolerates the ResultSort of S by PARTFUN1:59;
end;

theorem Th4:
  for x being set, S being non empty ManySortedSign st x in the carrier of S
  holds (SingleMSS x) +* S = the ManySortedSign of S
proof
  let x be set, S be non empty ManySortedSign;
  set T = (SingleMSS x) +* S;
  assume x in the carrier of S;
  then {x} c= the carrier of S by ZFMISC_1:31;
  then
A1: {x} \/ the carrier of S = the carrier of S by XBOOLE_1:12;
A2: {} \/ the carrier' of S = the carrier' of S;
A3: the carrier of SingleMSS x = {x} by Def1;
A4: the ResultSort of SingleMSS x = {};
A5: the Arity of SingleMSS x = {};
A6: {}+*the ResultSort of S = the ResultSort of S;
A7: {}+*the Arity of S = the Arity of S;
A8: the carrier of T = the carrier of S by A1,A3,CIRCCOMB:def 2;
A9: the carrier' of T = the carrier' of S by A2,A4,CIRCCOMB:def 2;
  the ResultSort of T = the ResultSort of S by A4,A6,CIRCCOMB:def 2;
  hence thesis by A5,A7,A8,A9,CIRCCOMB:def 2;
end;

theorem
  for x being set, S being non empty strict ManySortedSign
  for A being Boolean MSAlgebra over S st x in the carrier of S holds
  (SingleMSA x) +* A = the MSAlgebra of A
proof
  let x be set, S be non empty strict ManySortedSign;
  let A be Boolean MSAlgebra over S;
  set S1 = SingleMSS x, A1 = SingleMSA x;
  assume
A1: x in the carrier of S;
  then
A2: S1 +* S = S by Th4;
A3: {x} c= the carrier of S by A1,ZFMISC_1:31;
A4: the carrier of S1 = {x} by Def1;
A5: the Sorts of A = (the carrier of S) --> BOOLEAN by CIRCCOMB:57;
  the Sorts of A1 = (the carrier of S1) --> BOOLEAN by CIRCCOMB:57;
  then
A6: the Sorts of A1 tolerates the Sorts of A by A5,FUNCOP_1:87;
A7: the Charact of A = (the Charact of A1)+*the Charact of A;
A8: the Sorts of A1+*A = (the Sorts of A1)+*the Sorts of A by A6,CIRCCOMB:def 4
;
A9: the Charact of A = the Charact of A1+*A by A6,A7,CIRCCOMB:def 4;
A10: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
  dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
  hence thesis by A2,A3,A4,A8,A9,A10,FUNCT_4:19;
end;

notation
  synonym <*> for {};
end;

definition
  let n be Nat;
  let x,y be FinSequence;
A1: 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
  is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
  func n-BitAdderStr(x,y) ->
  unsplit gate`1=arity gate`2isBoolean non void strict
  non empty ManySortedSign means
  :Def3:
  ex f,g being ManySortedSet of NAT st
  it = f.n & f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  g.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
  for n being Nat, S being non empty ManySortedSign, z be set
  st S = f.n & z = g.n
  holds f.(n+1) = S +* BitAdderWithOverflowStr(x .(n+1), y.(n+1), z) &
  g.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z);
  uniqueness
  proof
    reconsider n as Element of NAT by ORDINAL1:def 12;
    deffunc o(set, Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
    deffunc S(non empty ManySortedSign, set, Nat) =
    $1 +* BitAdderWithOverflowStr(x .($3+1), y.($3+1), $2);
    for S1,S2 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)-->FALSE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
    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)-->FALSE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
    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
    reconsider n as Element of NAT by ORDINAL1:def 12;
    deffunc o(set, Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
    deffunc S(set, Nat)
    = BitAdderWithOverflowStr(x .($2+1), y.($2+1), $1);
    ex S 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)-->FALSE) &
    h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
    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-BitAdderCirc(x,y) ->
  Boolean gate`2=den strict Circuit of n-BitAdderStr(x,y) means
  :Def4:
  ex f,g,h being ManySortedSet of NAT st n-BitAdderStr(x,y) = f.n & it = g.n &
  f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
  for n 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 +* BitAdderWithOverflowStr(x .(n+1), y.(n+1), z) &
  g.(n+1) = A +* BitAdderWithOverflowCirc(x .(n+1), y.(n+1), z) &
  h.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z);
  uniqueness
  proof
    set S0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
    set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
    set Sn = n-BitAdderStr(x,y);
    set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
    deffunc o(set,Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
    deffunc S(non empty ManySortedSign, set, Nat) =
    $1 +* BitAdderWithOverflowStr(x .($3+1), y.($3+1), $2);
    deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
    set, Nat) = $2 +*
    BitAdderWithOverflowCirc(x .($4+1), y.($4+1), $3);
A1: for S 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
    n-BitAdderStr(x,y) 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)-->FALSE);
    set A0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE);
    set Sn = n-BitAdderStr(x,y);
    set o0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
    deffunc o(set,Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
    deffunc S(non empty ManySortedSign, set, Nat) =
    $1 +* BitAdderWithOverflowStr(x .($3+1), y.($3+1), $2);
    deffunc A(non empty ManySortedSign, non-empty MSAlgebra over $1,
    set, Nat) = $2 +*
    BitAdderWithOverflowCirc(x .($4+1), y.($4+1), $3);
A2: for S 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 Sn = f.n & f.0 = S0 & h.0 = o0 &
    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 Def3;
    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)-->FALSE];
  func n-BitMajorityOutput(x,y) ->
  Element of InnerVertices (n-BitAdderStr(x,y)) means
  :Def5:
  ex h being ManySortedSet of NAT st
  it = h.n & h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
  for n being Nat, z be set st z = h.n holds
  h.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z);
  uniqueness
  proof
    let o1, o2 be Element of InnerVertices (n-BitAdderStr(x,y));
    given h1 being ManySortedSet of NAT such that
A1: o1 = h1.n and
A2: h1.0 = c and
A3: for n being Nat, z be set st z = h1.n holds h1.(n+1) =
    MajorityOutput(x .(n+1), y.(n+1), z);
    given h2 being ManySortedSet of NAT such that
A4: o2 = h2.n and
A5: h2.0 = c and
A6: for n being Nat, z be set st z = h2.n holds h2.(n+1) =
    MajorityOutput(x .(n+1), y.(n+1), z);
    deffunc F(Nat,set) = MajorityOutput(x .($1+1), y.($1+1), $2);
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: h1.0 = c by A2;
A9: for n being Nat holds h1.(n+1) = F(n,h1.n) by A3;
A10: dom h2 = NAT by PARTFUN1:def 2;
A11: h2.0 = c by A5;
A12: for n being Nat holds h2.(n+1) = F(n,h2.n) by A6;
    h1 = h2 from NAT_1:sch 15(A7,A8,A9,A10,A11,A12);
    hence thesis by A1,A4;
  end;
  existence
  proof
    defpred P[set,set,set] means not contradiction;
    deffunc S(non empty ManySortedSign,set,Nat) =
    $1 +* BitAdderWithOverflowStr(x .($3+1), y.($3+1), $2);
    deffunc o(set,Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
    consider f,g being ManySortedSet of NAT such that
A13: n-BitAdderStr(x,y) = f.n and
A14: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A15: g.0 = c and
A16: for n 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 Def3;
    defpred P[Element of NAT] means
    ex S being non empty ManySortedSign st S = f.$1 & g.$1 in InnerVertices S;
    InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) = {c}
    by CIRCCOMB:42;
    then c in InnerVertices 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE)
    by TARSKI:def 1;
    then
A17: P[ 0 ] by A14,A15;
A18: for i being Element of NAT st P[i] holds P[i+1]
    proof
      let i be Element of NAT such that
A19:  ex S being non empty ManySortedSign st S = f.i & g.i in InnerVertices S
      and
A20:  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
A21:  S = f.i and g.i in InnerVertices S by A19;
      MajorityOutput(x .(i+1), y.(i+1), g.i) in
      InnerVertices BitAdderWithOverflowStr(x .(i+1), y.(i+1), g.i)
      by FACIRC_1:90;
      then
A22:  MajorityOutput(x .(i+1), y.(i+1), g.i) in InnerVertices (S+*
      BitAdderWithOverflowStr(x .(i+1), y.(i+1), g.i)) by FACIRC_1:22;
A23:  f.(i+1) = S +* BitAdderWithOverflowStr(x .(i+1), y.(i+1), g.i) by A16,A21
;
      g.(i+1) = MajorityOutput(x .(i+1), y.(i+1), g.i) by A16,A21;
      hence contradiction by A20,A22,A23;
    end;
    reconsider n9=n as Element of NAT by ORDINAL1:def 12;
    for i being Element of NAT holds P[i] from NAT_1:sch 1(A17,A18);
    then ex S being non empty ManySortedSign st S = f.n9 &
    g.n in InnerVertices S;
    then reconsider o = g.n9 as Element of InnerVertices (n-BitAdderStr(x,y))
    by A13;
    take o, g;
    thus o = g.n & g.0 = c by A15;
    let i be Nat;
A24: ex S being non empty ManySortedSign, x being set st
    S = f.0 & x = g.0 & P[S, x, 0] by A14;
A25: 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(A24,A16,A25);
    then ex S being non empty ManySortedSign st S = f.i;
    hence thesis by A16;
  end;
end;

theorem Th6:
  for x,y being FinSequence, f,g,h being ManySortedSet of NAT st
  f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] &
  for n 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 +* BitAdderWithOverflowStr(x .(n+1), y.(n+1), z) &
  g.(n+1) = A +* BitAdderWithOverflowCirc(x .(n+1), y.(n+1), z) &
  h.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z)
  for n being Nat holds
  n-BitAdderStr(x,y) = f.n & n-BitAdderCirc(x,y) = g.n &
  n-BitMajorityOutput(x,y) = h.n
proof
  let x,y be FinSequence, f,g,h be ManySortedSet of NAT;
  deffunc o(set,Nat) = MajorityOutput(x .($2+1), y.($2+1), $1);
  deffunc F(Nat,set) = MajorityOutput(x .($1+1), y.($1+1), $2);
  deffunc S(non empty ManySortedSign,set,Nat) =
  $1 +* BitAdderWithOverflowStr(x .($3+1), y.($3+1), $2);
  deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
  set,Nat) = $2 +*
  BitAdderWithOverflowCirc(x .($4+1), y.($4+1), $3);
  assume that
A1: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A2: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A3: for n 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-BitAdderStr(x,y) = f1.n and
A5: n-BitAdderCirc(x,y) = g1.n and
A6: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A7: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A8: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A9: for n 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 Def4;
  A10: ex
 S being non empty ManySortedSign, A being 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 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(A10,A11,A3,A9,A12
  );
  hence n-BitAdderStr(x,y) = f.n & n-BitAdderCirc(x,y) = g.n by A4,A5;
A13: 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,A12);
A14: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by A1;
A15: for n being Nat, z being set st z = h.n holds
  h.(n+1) = o(z,n) from CIRCCMB2:sch 3(A14,A13);
A16: dom h = NAT by PARTFUN1:def 2;
A17: h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] by A2;
  A18: for n being Nat holds h.(n+1) = F(n,h.n) by A15;
  consider h1 being ManySortedSet of NAT such that
A19: n-BitMajorityOutput(x,y) = h1.n and
A20: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A21: for n being Nat, z being set st z = h1.n holds h1.(n+1) =
  MajorityOutput(x .(n+1), y.(n+1), z)
  by Def5;
A22: dom h1 = NAT by PARTFUN1:def 2;
A23: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] by A20;
A24: for n being Nat holds h1.(n+1) = F(n,h1.n) by A21;
  h = h1 from NAT_1:sch 15(A16,A17,A18,A22,A23,A24);
  hence thesis by A19;
end;

theorem Th7:
  for a,b being FinSequence holds
  0-BitAdderStr(a,b) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  0-BitAdderCirc(a,b) = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) &
  0-BitMajorityOutput(a,b) = [<*>, (0-tuples_on BOOLEAN)-->FALSE]
proof
  let a,b be FinSequence;
A1: ex f,g,h being ManySortedSet of NAT st ( 0-BitAdderStr(a,b)
  = f.0)&( 0-BitAdderCirc(a,b) = g.0)&( f.0 = 1GateCircStr(<*>,(0-tuples_on
BOOLEAN)-->FALSE))&( g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE))&( h
.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE])&( for n 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 +* BitAdderWithOverflowStr(a .(n+1), b.(n+1
), z) & g.(n+1) = A +* BitAdderWithOverflowCirc(a .(n+1), b.(n+1), z) & h.(n+1)
  = MajorityOutput(a.(n+1), b.(n+1), z)) by Def4;
  hence
  0-BitAdderStr(a,b) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE);
  thus
  0-BitAdderCirc(a,b) = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) by A1;
  InnerVertices (0-BitAdderStr(a,b))
  = { [<*>,(0-tuples_on BOOLEAN)-->FALSE] } by A1,CIRCCOMB:42;
  hence thesis by TARSKI:def 1;
end;

theorem Th8:
  for a,b being FinSequence, c being set st
  c = [<*>, (0-tuples_on BOOLEAN)-->FALSE] holds
  1-BitAdderStr(a,b) = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->FALSE)+*
  BitAdderWithOverflowStr(a.1, b.1, c) &
  1-BitAdderCirc(a,b) = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->FALSE)+*
  BitAdderWithOverflowCirc(a.1, b.1, c) &
  1-BitMajorityOutput(a,b) = MajorityOutput(a.1, b.1, c)
proof
  let a,b being FinSequence, c be set such that
A1: c = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
  consider f,g,h being ManySortedSet of NAT such that
A2: 1-BitAdderStr(a,b) = f.1 and
A3: 1-BitAdderCirc(a,b) = g.1 and
A4: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A5: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A6: h.0 = c and
A7: for n 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+*BitAdderWithOverflowStr(a.(n+1),b.(n+1), z) &
  g.(n+1) = A+*BitAdderWithOverflowCirc(a.(n+1),b.(n+1), z) &
  h.(n+1) = MajorityOutput(a.(n+1), b.(n+1), z) by A1,Def4;
  1-BitMajorityOutput(a,b) = h.(0+1) by A1,A4,A5,A6,A7,Th6;
  hence thesis by A2,A3,A4,A5,A6,A7;
end;

theorem
  for a,b,c being set st c = [<*>, (0-tuples_on BOOLEAN)-->FALSE] holds
  1-BitAdderStr(<*a*>,<*b*>) =
  1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->FALSE)+*
  BitAdderWithOverflowStr(a, b, c) & 1-BitAdderCirc(<*a*>,<*b*>) =
  1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->FALSE)+*
  BitAdderWithOverflowCirc(a, b, c) &
  1-BitMajorityOutput(<*a*>,<*b*>) = MajorityOutput(a, b, c)
proof
  let a,b be set;
A1: <*a*>.1 = a by FINSEQ_1:40;
  <*b*>.1 = b by FINSEQ_1:40;
  hence thesis by A1,Th8;
end;

theorem Th10:
  for n be Element of NAT for p,q being FinSeqLen of n
  for p1,p2, q1,q2 being FinSequence holds
  n-BitAdderStr(p^p1, q^q1) = n-BitAdderStr(p^p2, q^q2) &
  n-BitAdderCirc(p^p1, q^q1) = n-BitAdderCirc(p^p2, q^q2) &
  n-BitMajorityOutput(p^p1, q^q1) = n-BitMajorityOutput(p^p2, q^q2)
proof
  let n be Element of NAT;
  set c = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
  let p,q be FinSeqLen of n;
  let p1,p2, q1,q2 be FinSequence;
  deffunc o(set,Nat) =
  MajorityOutput((p^p1) .($2+1), (q^q1).($2+1), $1);
  deffunc S(non empty ManySortedSign,set,Nat) =
  $1 +* BitAdderWithOverflowStr((p^p1) .($3+1), (q^q1).($3+1), $2);
  deffunc A(non empty ManySortedSign,non-empty MSAlgebra over $1,
  set,Nat) =
  $2 +* BitAdderWithOverflowCirc((p^p1) .($4+1), (q^q1).($4+1), $3);
  consider f1,g1,h1 being ManySortedSet of NAT such that
A1: n-BitAdderStr(p^p1,q^q1) = f1.n and
A2: n-BitAdderCirc(p^p1,q^q1) = g1.n and
A3: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A4: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A5: h1.0 = c and
A6: for n 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 Def4;
  consider f2,g2,h2 being ManySortedSet of NAT such that
A7: n-BitAdderStr(p^p2,q^q2) = f2.n and
A8: n-BitAdderCirc(p^p2,q^q2) = g2.n and
A9: f2.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A10: g2.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A11: h2.0 = c and
A12: for n 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 +* BitAdderWithOverflowStr((p^p2).(n+1), (q^q2).(n+1), z) &
  g2.(n+1) = A +* BitAdderWithOverflowCirc((p^p2).(n+1), (q^q2).(n+1), z) &
  h2.(n+1) = MajorityOutput((p^p2).(n+1), (q^q2).(n+1), z) by Def4;
  defpred L[Nat] means
  $1 <= n implies h1.$1 = h2.$1 & f1.$1 = f2.$1 & g1.$1 = g2.$1;
A13: L[ 0 ] by A3,A4,A5,A9,A10,A11;
A14: for i being 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 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 A3,A4;
A27: 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];
A28: 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(A26,A6,A27,A28);
    then consider S being non empty ManySortedSign,
    A being non-empty MSAlgebra over S such that
A29: S = f1.i and
A30: A = g1.i;
    thus h1.(i+1)
    = MajorityOutput((p^p2).(i+1), (q^q2).(i+1), h2.i) by A6,A15,A16,A22,A23
,A24,A25,A29,A30,NAT_1:13
      .= h2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
    thus f1.(i+1)
    = S+*BitAdderWithOverflowStr((p^p2).(i+1), (q^q2).(i+1), h2.i)
    by A6,A15,A16,A22,A23,A24,A25,A29,A30,NAT_1:13
      .= f2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
    thus g1.(i+1)
    = A+*BitAdderWithOverflowCirc((p^p2).(i+1), (q^q2).(i+1), h2.i)
    by A6,A15,A16,A22,A23,A24,A25,A29,A30,NAT_1:13
      .= g2.(i+1) by A12,A15,A16,A29,A30,NAT_1:13;
  end;
A31: for i being Nat holds L[i] from NAT_1:sch 2(A13,A14);
  hence n-BitAdderStr(p^p1, q^q1) = n-BitAdderStr(p^p2, q^q2) &
  n-BitAdderCirc(p^p1, q^q1) = n-BitAdderCirc(p^p2, q^q2) by A1,A2,A7,A8;
A32: n-BitMajorityOutput(p^p1, q^q1) = h1.n by A3,A4,A5,A6,Th6;
  n-BitMajorityOutput(p^p2, q^q2) = h2.n by A9,A10,A11,A12,Th6;
  hence thesis by A31,A32;
end;

theorem
  for n be Element of NAT for x,y being FinSeqLen of n for a,b being set holds
  (n+1)-BitAdderStr(x^<*a*>, y^<*b*>) = n-BitAdderStr(x, y) +*
  BitAdderWithOverflowStr(a, b, n-BitMajorityOutput(x, y)) &
  (n+1)-BitAdderCirc(x^<*a*>, y^<*b*>) = n-BitAdderCirc(x, y) +*
  BitAdderWithOverflowCirc(a, b, n-BitMajorityOutput(x, y)) &
  (n+1)-BitMajorityOutput(x^<*a*>, y^<*b*>) =
  MajorityOutput(a, b, n-BitMajorityOutput(x, y))
proof
  let n be Element of NAT;
  set c = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
  let x,y be FinSeqLen of n;
  let a,b be set;
  set p = x^<*a*>, q = y^<*b*>;
  consider f,g,h being ManySortedSet of NAT such that
A1: n-BitAdderStr(p,q) = f.n and
A2: n-BitAdderCirc(p,q) = g.n and
A3: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A4: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A5: h.0 = c and
A6: for n 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 +* BitAdderWithOverflowStr(p.(n+1), q.(n+1), z) &
  g.(n+1) = A +* BitAdderWithOverflowCirc(p.(n+1), q.(n+1), z) &
  h.(n+1) = MajorityOutput(p.(n+1), q.(n+1), z) by Def4;
A7: n-BitMajorityOutput(x^<*a*>, y^<*b*>) = h.n by A3,A4,A5,A6,Th6;
A8: (n+1)-BitAdderStr(x^<*a*>, y^<*b*>) = f.(n+1) by A3,A4,A5,A6,Th6;
A9: (n+1)-BitAdderCirc(x^<*a*>, y^<*b*>) = g.(n+1) by A3,A4,A5,A6,Th6;
A10: (n+1)-BitMajorityOutput(x^<*a*>, y^<*b*>) = h.(n+1) by A3,A4,A5,A6,Th6;
A11: len x = n by CARD_1:def 7;
A12: len y = n by CARD_1:def 7;
A13: p.(n+1) = a by A11,FINSEQ_1:42;
A14: q.(n+1) = b by A12,FINSEQ_1:42;
A15: x^<*> = x by FINSEQ_1:34;
A16: y^<*> = y by FINSEQ_1:34;
  then
A17: n-BitAdderStr(p, q) = n-BitAdderStr(x, y) by A15,Th10;
A18: n-BitAdderCirc(p, q) = n-BitAdderCirc(x, y) by A15,A16,Th10;
  n-BitMajorityOutput(p, q) = n-BitMajorityOutput(x, y) by A15,A16,Th10;
  hence thesis by A1,A2,A6,A7,A8,A9,A10,A13,A14,A17,A18;
end;

theorem Th12:
  for n be Element of NAT for x,y being FinSequence holds
  (n+1)-BitAdderStr(x, y) = n-BitAdderStr(x, y) +*
  BitAdderWithOverflowStr(x .(n+1), y.(n+1), n-BitMajorityOutput(x, y)) &
  (n+1)-BitAdderCirc(x, y) = n-BitAdderCirc(x, y) +*
  BitAdderWithOverflowCirc(x .(n+1), y.(n+1), n-BitMajorityOutput(x, y)) &
  (n+1)-BitMajorityOutput(x, y) =
  MajorityOutput(x .(n+1), y.(n+1), n-BitMajorityOutput(x, y))
proof
  let n be Element of NAT;
  let x,y be FinSequence;
  set c = [<*>, (0-tuples_on BOOLEAN)-->FALSE];
  consider f,g,h being ManySortedSet of NAT such that
A1: n-BitAdderStr(x,y) = f.n and
A2: n-BitAdderCirc(x,y) = g.n and
A3: f.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A4: g.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A5: h.0 = c and
A6: for n 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 +* BitAdderWithOverflowStr(x .(n+1), y.(n+1), z) &
  g.(n+1) = A +* BitAdderWithOverflowCirc(x .(n+1), y.(n+1), z) &
  h.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z) by Def4;
A7: n-BitMajorityOutput(x, y) = h.n by A3,A4,A5,A6,Th6;
A8: (n+1)-BitAdderStr(x, y) = f.(n+1) by A3,A4,A5,A6,Th6;
A9: (n+1)-BitAdderCirc(x, y) = g.(n+1) by A3,A4,A5,A6,Th6;
  (n+1)-BitMajorityOutput(x, y) = h.(n+1) by A3,A4,A5,A6,Th6;
  hence thesis by A1,A2,A6,A7,A8,A9;
end;

theorem Th13:
  for n,m be Element of NAT st n <= m for x,y being FinSequence holds
  InnerVertices (n-BitAdderStr(x,y)) c= InnerVertices (m-BitAdderStr(x,y))
proof
  let n,m be Element of NAT such that
A1: n <= m;
  let x,y be FinSequence;
  consider i being Nat such that
A2: m = n+i by A1,NAT_1:10;
  reconsider i as Element of NAT by ORDINAL1:def 12;
A3: m = n+i by A2;
  defpred L[Element of NAT] means InnerVertices (n-BitAdderStr(x,y)) c=
  InnerVertices ((n+$1)-BitAdderStr(x,y));
A4: L[ 0 ];
A5: for j being Element of NAT st L[j] holds L[j+1]
  proof
    let j be Element of NAT;
    assume
A6: InnerVertices (n-BitAdderStr(x,y)) c=
    InnerVertices ((n+j)-BitAdderStr(x,y));
A7: ((n+j)+1)-BitAdderStr(x,y) = (n+j)-BitAdderStr(x,y) +*
    BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y)) by Th12;
A8: InnerVertices (((n+j)-BitAdderStr(x,y) +*
    BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y))))
    = InnerVertices ((n+j)-BitAdderStr(x,y)) \/
    InnerVertices (BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y))) by FACIRC_1:27;
A9: InnerVertices (n-BitAdderStr(x,y)) c= InnerVertices (n-BitAdderStr(x,y)) \/
    InnerVertices (BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y))) by XBOOLE_1:7;
    InnerVertices (n-BitAdderStr(x,y)) \/
    InnerVertices (BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y))) c=
    InnerVertices ((n+j)-BitAdderStr(x,y)) \/
    InnerVertices (BitAdderWithOverflowStr(x .((n+j)+1), y.((n+j)+1),
    (n+j)-BitMajorityOutput(x, y))) by A6,XBOOLE_1:9;
    hence thesis by A7,A8,A9,XBOOLE_1:1;
  end;
  for j being Element of NAT holds L[j] from NAT_1:sch 1(A4,A5);
  hence thesis by A3;
end;

theorem
  for n be Element of NAT for x,y being FinSequence holds
  InnerVertices ((n+1)-BitAdderStr(x,y)) =
  InnerVertices (n-BitAdderStr(x,y)) \/
  InnerVertices BitAdderWithOverflowStr(x .(n+1), y.(n+1),
  n-BitMajorityOutput(x,y))
proof
  let n be Element of NAT;
  let x,y be FinSequence;
  (n+1)-BitAdderStr(x,y) = n-BitAdderStr(x,y) +*
  BitAdderWithOverflowStr(x .(n+1), y.(n+1),
  n-BitMajorityOutput(x, y)) by Th12;
  hence thesis by FACIRC_1:27;
end;

definition
  let k,n be Nat such that
X1: k >= 1 and
X2: k <= n;
  let x,y be FinSequence;
  func (k,n)-BitAdderOutput(x,y) ->
  Element of InnerVertices (n-BitAdderStr(x,y)) means
  :Def6:
  ex i being Element of NAT st k = i+1 &
  it = BitAdderOutput(x .k, y.k, i-BitMajorityOutput(x,y));
  uniqueness;
  existence
  proof consider i being Nat such that
A1: k = 1+i by X1,NAT_1:10;
    reconsider n9=n,k9=k,i as Element of NAT by ORDINAL1:def 12;
    set o = BitAdderOutput(x .k, y.k, i-BitMajorityOutput(x,y));
    A2: InnerVertices
 (k9-BitAdderStr(x,y)) c= InnerVertices (n9-BitAdderStr(x,y))
    by X2,Th13;
A3: o in InnerVertices BitAdderWithOverflowStr(x .(i+1), y.(i+1),
    i-BitMajorityOutput(x, y)) by A1,FACIRC_1:90;
A4: k-BitAdderStr(x,y) = (i-BitAdderStr(x, y)) +*
    BitAdderWithOverflowStr(x .(i+1), y.(i+1), i-BitMajorityOutput(x, y))
    by A1,Th12;
    reconsider o as Element of
    BitAdderWithOverflowStr(x .(i+1), y.(i+1), i-BitMajorityOutput(x, y))
    by A3;
    (the carrier of
    BitAdderWithOverflowStr(x .(i+1), y.(i+1), i-BitMajorityOutput(x, y)))
    \/ the carrier of i-BitAdderStr(x,y)
    = the carrier of k-BitAdderStr(x,y) by A4,CIRCCOMB:def 2;
    then o in the carrier of k-BitAdderStr(x,y) by XBOOLE_0:def 3;
    then o in InnerVertices (k-BitAdderStr(x,y)) by A3,A4,CIRCCOMB:15;
    hence thesis by A1,A2;
  end;
end;

theorem
  for n,k being Element of NAT st k < n for x,y being FinSequence holds
  (k+1,n)-BitAdderOutput(x,y) =
  BitAdderOutput(x .(k+1), y.(k+1), k-BitMajorityOutput(x,y))
proof
  let n,k be Element of NAT such that
A1: k < n;
  let x,y be FinSequence;
A2: k+1 >= 1 by NAT_1:11;
  k+1 <= n by A1,NAT_1:13;
  then ex i being Element of NAT st ( k+1 = i+1)&( (k+1,n)
-BitAdderOutput(x,y) = BitAdderOutput(x .(k+1), y.(k+1), i -BitMajorityOutput(x
  ,y))) by A2,Def6;
  hence thesis;
end;

Lm1: now
  let i be Element of NAT;
  let x be FinSeqLen of i+1;
A1: len x = i+1 by CARD_1:def 7;
  then x <> <*>;
  then consider y being FinSequence, a being set such that
A2: x = y^<*a*> by FINSEQ_1:46;
  len <*a*> = 1 by FINSEQ_1:40;
  then i+1 = len y+1 by A1,A2,FINSEQ_1:22;
  then reconsider y as FinSeqLen of i by CARD_1:def 7;
  take y, a;
  thus x = y^<*a*> by A2;
end;

Lm2: now
  let i be Element of NAT;
  let x be nonpair-yielding FinSeqLen of i+1;
  consider y being FinSeqLen of i, a being set such that
A1: x = y^<*a*> by Lm1;
A2: dom y c= dom x by A1,FINSEQ_1:26;
A3: y = x|dom y by A1,FINSEQ_1:21;
  y is nonpair-yielding
  proof
    let z be set;
    assume
A4: z in dom y;
    then y.z = x .z by A3,FUNCT_1:47;
    hence thesis by A2,A4,FACIRC_1:def 3;
  end;
  then reconsider y as nonpair-yielding FinSeqLen of i;
A5: i+1 in Seg (i+1) by FINSEQ_1:4;
  dom x = Seg len x by FINSEQ_1:def 3;
  then
A6: i+1 in dom x by A5,CARD_1:def 7;
A7: x .(len y+1) = a by A1,FINSEQ_1:42;
  len y = i by CARD_1:def 7;
  then reconsider a as non pair set by A6,A7,FACIRC_1:def 3;
  take y, a;
  thus x = y^<*a*> by A1;
end;

theorem
  for n being Element of NAT for x,y being FinSequence holds
  InnerVertices (n-BitAdderStr(x,y)) is Relation
proof
  let n be Element of NAT;
  let x,y be FinSequence;
  defpred P[Element of NAT] means
  InnerVertices ($1-BitAdderStr(x,y)) is Relation;
  0-BitAdderStr(x,y) = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) by Th7;
  then
A1: P[ 0 ] by FACIRC_1:38;
A2: for i being Element of NAT st P[i] holds P[i+1]
  proof
    let i be Element of NAT;
    assume
A3: InnerVertices (i-BitAdderStr(x,y)) is Relation;
A4: (i+1)-BitAdderStr(x, y) = i-BitAdderStr(x, y) +*
    BitAdderWithOverflowStr(x .(i+1), y.(i+1),
    i-BitMajorityOutput(x, y)) by Th12;
    InnerVertices BitAdderWithOverflowStr(x .(i+1), y.(i+1),
    i-BitMajorityOutput(x, y)) is Relation by FACIRC_1:88;
    hence thesis by A3,A4,FACIRC_1:3;
  end;
  for i being Element of NAT holds P[i] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th17:
  for x,y,c being set holds InnerVertices MajorityIStr(x,y,c) =
  {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']}
proof
  let x,y,c be set;
A1: 1GateCircStr(<*x,y*>,'&') +* 1GateCircStr(<*y,c*>,'&') tolerates
  1GateCircStr(<*c,x*>,'&') by CIRCCOMB:47;
A2: 1GateCircStr(<*x,y*>,'&') tolerates 1GateCircStr(<*y,c*>,'&')
  by CIRCCOMB:47;
  InnerVertices MajorityIStr(x,y,c) =
  InnerVertices(1GateCircStr(<*x,y*>,'&') +* 1GateCircStr(<*y,c*>,'&')) \/
  InnerVertices(1GateCircStr(<*c,x*>,'&')) by A1,CIRCCOMB:11
    .= InnerVertices(1GateCircStr(<*x,y*>,'&')) \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')) \/
  InnerVertices(1GateCircStr(<*c,x*>,'&')) by A2,CIRCCOMB:11
    .= {[<*x,y*>,'&']} \/ InnerVertices(1GateCircStr(<*y,c*>,'&')) \/
  InnerVertices(1GateCircStr(<*c,x*>,'&')) by CIRCCOMB:42
    .= {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/
  InnerVertices(1GateCircStr(<*c,x*>,'&')) by CIRCCOMB:42
    .= {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by CIRCCOMB:42
    .= {[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
    .= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by ENUMSET1:3;
  hence thesis;
end;

theorem Th18:
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&']
  holds InputVertices MajorityIStr(x,y,c) = {x,y,c}
proof
  let x,y,c be set;
  assume that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'];
A4: 1GateCircStr(<*x,y*>,'&') tolerates 1GateCircStr(<*y,c*>,'&')
  by CIRCCOMB:47;
A5: y in {1,y} by TARSKI:def 2;
A6: y in {2,y} by TARSKI:def 2;
A7: {1,y} in [1,y] by TARSKI:def 2;
A8: {2,y} in [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*>,'&'] by TARSKI:def 2;
  then
A13: y <> [<*y,c*>,'&'] by A5,A7,A9,A10,A11,XREGULAR:9;
A14: c in {2,c} by TARSKI:def 2;
A15: {2,c} in [2,c] by TARSKI:def 2;
  dom<*y,c*> = Seg 2 by FINSEQ_1:89;
  then
A16: 2 in dom <*y,c*> by FINSEQ_1:1;
  <*y,c*>.2 = c by FINSEQ_1:44;
  then [2,c] in <*y,c*> by A16,FUNCT_1:1;
  then
A17: c <> [<*y,c*>,'&'] by A11,A12,A14,A15,XREGULAR:9;
  dom<*x,y*> = Seg 2 by FINSEQ_1:89;
  then
A18: 2 in dom <*x,y*> by FINSEQ_1:1;
  <*x,y*>.2 = y by FINSEQ_1:44;
  then
A19: [2,y] in <*x,y*> by A18,FUNCT_1:1;
A20: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
  {<*x,y*>} in [<*x,y*>,'&'] by TARSKI:def 2;
  then y <> [<*x,y*>,'&'] by A6,A8,A19,A20,XREGULAR:9;
  then
A21: not [<*x,y*>,'&'] in {y,c} by A3,TARSKI:def 2;
A22: x in {1,x} by TARSKI:def 2;
A23: {1,x} in [1,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*>,'&'] by TARSKI:def 2;
  then
A27: x <> [<*x,y*>,'&'] by A22,A23,A24,A25,A26,XREGULAR:9;
A28: not c in {[<*x,y*>,'&'], [<*y,c*>,'&']} by A3,A17,TARSKI:def 2;
A29: not x in {[<*x,y*>,'&'], [<*y,c*>,'&']} by A1,A27,TARSKI:def 2;
A30: x in {2,x} by TARSKI:def 2;
A31: {2,x} in [2,x] by TARSKI:def 2;
  dom<*c,x*> = Seg 2 by FINSEQ_1:89;
  then
A32: 2 in dom <*c,x*> by FINSEQ_1:1;
  <*c,x*>.2 = x by FINSEQ_1:44;
  then
A33: [2,x] in <*c,x*> by A32,FUNCT_1:1;
A34: <*c,x*> in {<*c,x*>} by TARSKI:def 1;
  {<*c,x*>} in [<*c,x*>,'&'] by TARSKI:def 2;
  then
A35: x <> [<*c,x*>,'&'] by A30,A31,A33,A34,XREGULAR:9;
A36: c in {1,c} by TARSKI:def 2;
A37: {1,c} in [1,c] by TARSKI:def 2;
  <*c,x*> = <*c*>^<*x*> by FINSEQ_1:def 9;
  then
A38: <*c*> c= <*c,x*> by FINSEQ_6:10;
  <*c*> = {[1,c]} by FINSEQ_1:def 5;
  then
A39: [1,c] in <*c*> by TARSKI:def 1;
A40: <*c,x*> in {<*c,x*>} by TARSKI:def 1;
  {<*c,x*>} in [<*c,x*>,'&'] by TARSKI:def 2;
  then c <> [<*c,x*>,'&'] by A36,A37,A38,A39,A40,XREGULAR:9;
  then
A41: not [<*c,x*>,'&'] in {x,y,c} by A2,A35,ENUMSET1:def 1;
  InputVertices MajorityIStr(x,y,c)
  = (InputVertices(1GateCircStr(<*x,y*>,'&') +* 1GateCircStr(<*y,c*>,'&')) \
  InnerVertices(1GateCircStr(<*c,x*>,'&'))) \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  InnerVertices(1GateCircStr(<*x,y*>,'&') +*
  1GateCircStr(<*y,c*>,'&'))) by CIRCCMB2:5,CIRCCOMB:47
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \
  InnerVertices(1GateCircStr(<*y,c*>,'&'))) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  InnerVertices(1GateCircStr(<*x,y*>,'&')))) \
  InnerVertices(1GateCircStr(<*c,x*>,'&')) \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  InnerVertices(1GateCircStr(<*x,y*>,'&') +*
  1GateCircStr(<*y,c*>,'&'))) by CIRCCMB2:5,CIRCCOMB:47
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \
  InnerVertices(1GateCircStr(<*y,c*>,'&'))) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  InnerVertices(1GateCircStr(<*x,y*>,'&')))) \
  InnerVertices(1GateCircStr(<*c,x*>,'&')) \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  (InnerVertices(1GateCircStr(<*x,y*>,'&')) \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')))) by A4,CIRCCOMB:11
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \ {[<*y,c*>,'&']}) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  InnerVertices(1GateCircStr(<*x,y*>,'&')))) \
  InnerVertices(1GateCircStr(<*c,x*>,'&')) \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  (InnerVertices(1GateCircStr(<*x,y*>,'&')) \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')))) by CIRCCOMB:42
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \ {[<*y,c*>,'&']}) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \ {[<*x,y*>,'&']})) \
  InnerVertices(1GateCircStr(<*c,x*>,'&')) \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  (InnerVertices(1GateCircStr(<*x,y*>,'&')) \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')))) by CIRCCOMB:42
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \ {[<*y,c*>,'&']}) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']} \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  (InnerVertices(1GateCircStr(<*x,y*>,'&')) \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')))) by CIRCCOMB:42
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \ {[<*y,c*>,'&']}) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']} \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \ ({[<*x,y*>,'&']} \/
  InnerVertices(1GateCircStr(<*y,c*>,'&')))) by CIRCCOMB:42
    .= ((InputVertices(1GateCircStr(<*x,y*>,'&')) \ {[<*y,c*>,'&']}) \/
  (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']} \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by CIRCCOMB:42
    .= (({x,y} \
  {[<*y,c*>,'&']}) \/ (InputVertices(1GateCircStr(<*y,c*>,'&')) \
  {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']} \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
    .=(({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \
  {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']} \/
  (InputVertices(1GateCircStr(<*c,x*>,'&')) \
  ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
    .=(({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \ {[<*x,y*>,'&']})) \
  {[<*c,x*>,'&']} \/
  ({c,x} \ ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
    .= (({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \ {[<*x,y*>,'&']})) \
  {[<*c,x*>,'&']} \/ ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by ENUMSET1:1
    .= (({x,y} \/ ({y,c} \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/
  ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by A1,A13,Th1
    .= ({x,y} \/ {y,c}) \ {[<*c,x*>,'&']} \/
  ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by A21,ZFMISC_1:57
    .= ({x,y} \/ {y,c}) \ {[<*c,x*>,'&']} \/ {c,x} by A28,A29,ZFMISC_1:63
    .= {x,y,y,c} \ {[<*c,x*>,'&']} \/ {c,x} by ENUMSET1:5
    .= {y,y,x,c} \ {[<*c,x*>,'&']} \/ {c,x} by ENUMSET1:67
    .= {y,x,c} \ {[<*c,x*>,'&']} \/ {c,x} by ENUMSET1:31
    .= {x,y,c} \ {[<*c,x*>,'&']} \/ {c,x} by ENUMSET1:58
    .= {x,y,c} \/ {c,x} by A41,ZFMISC_1:57
    .= {x,y,c,c,x} by ENUMSET1:9
    .= {x,y,c,c} \/ {x} by ENUMSET1:10
    .= {c,c,x,y} \/ {x} by ENUMSET1:73
    .= {c,x,y} \/ {x} by ENUMSET1:31
    .= {c,x,y,x} by ENUMSET1:6
    .= {x,x,y,c} by ENUMSET1:70
    .= {x,y,c} by ENUMSET1:31;
  hence thesis;
end;

theorem Th19:
  for x,y,c being set holds InnerVertices MajorityStr(x,y,c) =
  {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
proof
  let x,y,c be set;
  set xy = [<*x,y*>, '&'], yc = [<*y,c*>, '&'], cx = [<*c,x*>, '&'];
  set Cxy = 1GateCircStr(<*x,y*>, '&'), Cyc = 1GateCircStr(<*y,c*>, '&'),
  Ccx = 1GateCircStr(<*c,x*>, '&'), Cxyc = 1GateCircStr
  (<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
A1: Cxy tolerates (Cyc +* Ccx +* Cxyc) by CIRCCOMB:47;
A2: Cyc tolerates (Ccx +* Cxyc) by CIRCCOMB:47;
A3: Ccx tolerates Cxyc by CIRCCOMB:47;
A4: InnerVertices (Cyc +* (Ccx +* Cxyc)) =
  InnerVertices Cyc \/ InnerVertices (Ccx +* Cxyc) by A2,CIRCCOMB:11;
A5: InnerVertices (Ccx +* Cxyc) =
  InnerVertices Ccx \/ InnerVertices Cxyc by A3,CIRCCOMB:11;
  thus
  InnerVertices MajorityStr(x,y,c) =
  InnerVertices (Cxy +* (Cyc +* Ccx) +* Cxyc) by CIRCCOMB:6
    .= InnerVertices (Cxy +* (Cyc +* Ccx +* Cxyc)) by CIRCCOMB:6
    .= InnerVertices Cxy \/ InnerVertices (Cyc +* Ccx +* Cxyc)
  by A1,CIRCCOMB:11
    .= InnerVertices Cxy \/ InnerVertices (Cyc +* (Ccx +* Cxyc))
  by CIRCCOMB:6
    .= InnerVertices Cxy \/ InnerVertices Cyc \/
  (InnerVertices Ccx \/ InnerVertices Cxyc) by A4,A5,XBOOLE_1:4
    .= InnerVertices Cxy \/ InnerVertices Cyc \/
  InnerVertices Ccx \/ InnerVertices Cxyc by XBOOLE_1:4
    .= {xy} \/ InnerVertices Cyc \/
  InnerVertices Ccx \/ InnerVertices Cxyc by CIRCCOMB:42
    .= {xy} \/ {yc} \/ InnerVertices Ccx \/ InnerVertices Cxyc by CIRCCOMB:42
    .= {xy} \/ {yc} \/ {cx} \/ InnerVertices Cxyc by CIRCCOMB:42
    .= {xy, yc} \/ {cx} \/ InnerVertices Cxyc by ENUMSET1:1
    .= {xy, yc, cx} \/ InnerVertices Cxyc by ENUMSET1:3
    .= {xy, yc, cx} \/ {MajorityOutput(x,y,c)} by CIRCCOMB:42;
end;

theorem Th20:
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&']
  holds InputVertices MajorityStr(x,y,c) = {x,y,c}
proof
  let x,y,c be set;
  set xy = [<*x,y*>, '&'], yc = [<*y,c*>, '&'], cx = [<*c,x*>, '&'];
  set S = 1GateCircStr(<*xy, yc, cx*>, or3);
A1: InnerVertices S = {[<*xy, yc, cx*>, or3]} by CIRCCOMB:42;
A2: InputVertices S = rng <*xy, yc, cx*> by CIRCCOMB:42
    .= {xy, yc, cx} by FINSEQ_2:128;
  set MI = MajorityIStr(x,y,c);
  assume that
A3: x <> yc and
A4: y <> cx and
A5: c <> xy;
  rng <*c,x*> = {c,x} by FINSEQ_2:127;
  then
A6: x in rng <*c,x*> by TARSKI:def 2;
  len <*xy, yc, cx*> = 3 by FINSEQ_1:45;
  then
A7: Seg 3 = dom <*xy, yc, cx*> by FINSEQ_1:def 3;
  then
A8: 3 in dom <*xy, yc, cx*> by FINSEQ_1:1;
  <*xy, yc, cx*>.3 = cx by FINSEQ_1:45;
  then [3,cx] in <*xy, yc, cx*> by A8,FUNCT_1:1;
  then cx in rng <*xy, yc, cx*> by XTUPLE_0:def 13;
  then
A9: the_rank_of cx in the_rank_of [<*xy, yc, cx*>, or3] by CLASSES1:82;
  rng <*x,y*> = {x,y} by FINSEQ_2:127;
  then
A10: y in rng <*x,y*> by TARSKI:def 2;
A11: 1 in dom <*xy, yc, cx*> by A7,FINSEQ_1:1;
  <*xy, yc, cx*>.1 = xy by FINSEQ_1:45;
  then [1,xy] in <*xy, yc, cx*> by A11,FUNCT_1:1;
  then xy in rng <*xy, yc, cx*> by XTUPLE_0:def 13;
  then
A12: the_rank_of xy in the_rank_of [<*xy, yc, cx*>, or3] by CLASSES1:82;
  rng <*y,c*> = {y,c} by FINSEQ_2:127;
  then
A13: c in rng <*y,c*> by TARSKI:def 2;
A14: 2 in dom <*xy, yc, cx*> by A7,FINSEQ_1:1;
  <*xy, yc, cx*>.2 = yc by FINSEQ_1:45;
  then [2,yc] in <*xy, yc, cx*> by A14,FUNCT_1:1;
  then yc in rng <*xy, yc, cx*> by XTUPLE_0:def 13;
  then
A15: the_rank_of yc in the_rank_of [<*xy, yc, cx*>, or3] by CLASSES1:82;
A16: {xy, yc, cx} \ {xy, yc, cx} = {} by XBOOLE_1:37;
A17: {x, y, c} \ {[<*xy, yc, cx*>, or3]} = {x, y, c}
  proof
    thus {x,y,c} \ {[<*xy, yc, cx*>, or3]} c= {x,y,c};
    let a be set;
    assume
A18: a in {x,y,c};
    then a = x or a = y or a = c by ENUMSET1:def 1;
    then a <> [<*xy, yc, cx*>, or3] by A6,A9,A10,A12,A13,A15,CLASSES1:82;
    then not a in {[<*xy, yc, cx*>, or3]} by TARSKI:def 1;
    hence thesis by A18,XBOOLE_0:def 5;
  end;
  thus InputVertices MajorityStr(x,y,c)
  = ((InputVertices MI) \ InnerVertices S) \/
  ((InputVertices S) \ InnerVertices MI) by CIRCCMB2:5,CIRCCOMB:47
    .= {x,y,c} \/ ({xy, yc, cx} \ InnerVertices MI) by A1,A2,A3,A4,A5,A17,Th18
    .= {x,y,c} \/ {} by A16,Th17
    .= {x,y,c};
end;

theorem Th21:
  for S1,S2 being non empty ManySortedSign
  st S1 tolerates S2 & InputVertices S1 = InputVertices S2
  holds InputVertices (S1+*S2) = InputVertices S1
proof
  let S1,S2 be non empty ManySortedSign such that
A1: S1 tolerates S2 and
A2: InputVertices S1 = InputVertices S2;
A3: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A4: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
  thus
  InputVertices (S1+*S2) = ((InputVertices S1)\(InnerVertices S2)) \/
  ((InputVertices S2)\(InnerVertices S1)) by A1,CIRCCMB2:5
    .= (InputVertices S1) \/
  ((InputVertices S2)\(InnerVertices S1)) by A2,A4,XBOOLE_1:83
    .= InputVertices S1 \/ InputVertices S2 by A2,A3,XBOOLE_1:83
    .= InputVertices S1 by A2;
end;

theorem Th22:
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&'] &
  c <> [<*x,y*>, 'xor'] holds
  InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c}
proof
  let x,y,c be set such that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'] and
A4: c <> [<*x,y*>, 'xor'];
A5: InputVertices 2GatesCircStr(x,y,c, 'xor') = {x,y,c} by A4,FACIRC_1:57;
  InputVertices MajorityStr(x,y,c) = {x,y,c} by A1,A2,A3,Th20;
  hence thesis by A5,Th21,CIRCCOMB:47;
end;

theorem Th23:
  for x,y,c being set holds InnerVertices BitAdderWithOverflowStr(x,y,c) =
  {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
  {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
proof
  let x,y,c be set;
  2GatesCircStr(x,y,c, 'xor') tolerates MajorityStr(x,y,c) by CIRCCOMB:47;
  then InnerVertices BitAdderWithOverflowStr(x,y,c) =
  InnerVertices 2GatesCircStr(x,y,c, 'xor') \/
  InnerVertices MajorityStr(x,y,c) by CIRCCOMB:11
    .= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
  InnerVertices MajorityStr(x,y,c) by FACIRC_1:56
    .= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
  ({[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
  {MajorityOutput(x,y,c)}) by Th19
    .= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
  {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
  by XBOOLE_1:4;
  hence thesis;
end;

registration
  cluster empty -> non pair for set;
  coherence;
end;

registration
  cluster empty -> nonpair-yielding for Function;
  coherence
  proof
    let F be Function such that
A1: F is empty;
    let x be set;
    assume x in dom F;
    thus thesis by A1;
  end;
  let f be nonpair-yielding Function;
  let x be set;
  cluster f.x -> non pair;
  coherence
  proof per cases;
    suppose x in dom f;
      hence thesis by FACIRC_1:def 3;
    end;
    suppose not x in dom f;
      hence thesis by FUNCT_1:def 2;
    end;
  end;
end;

registration
  let n be Element of NAT;
  let x,y be FinSequence;
  cluster n-BitMajorityOutput(x,y) -> pair;
  coherence
  proof
A1: ex h being ManySortedSet of NAT st ( 0-BitMajorityOutput(x,
y) = h.0)&( h.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE])&( for n being Nat, z be
set st z = h.n holds h.(n+1) = MajorityOutput(x .(n+1), y.(n+1), z)) by Def5;
    defpred P[Element of NAT] means $1-BitMajorityOutput(x,y) is pair;
A2: P[ 0 ] by A1;
A3: for n being Element of NAT st P[n] holds P[n+1]
    proof
      let n be Element of NAT;
      (n+1)-BitMajorityOutput(x, y) =
      MajorityOutput(x .(n+1), y.(n+1), n-BitMajorityOutput(x, y)) by Th12
        .= [<*[<*x .(n+1),y.(n+1)*>, '&'],
      [<*y.(n+1),n-BitMajorityOutput(x, y)*>, '&'],
      [<*n-BitMajorityOutput(x, y),x .(n+1)*>, '&']*>, or3];
      hence thesis;
    end;
    for n being Element of NAT holds P[n] from NAT_1:sch 1(A2,A3);
    hence thesis;
  end;
end;

theorem Th24:
  for x,y being FinSequence, n being Element of NAT holds
  (n-BitMajorityOutput(x,y))`1 = <*> &
  (n-BitMajorityOutput(x,y))`2 = (0-tuples_on BOOLEAN)-->FALSE &
  proj1 (n-BitMajorityOutput(x,y))`2 = 0-tuples_on BOOLEAN or
  card (n-BitMajorityOutput(x,y))`1 = 3 & (n-BitMajorityOutput(x,y))`2 = or3 &
  proj1 (n-BitMajorityOutput(x,y))`2 = 3-tuples_on BOOLEAN
proof
  let x,y be FinSequence;
  defpred P[Element of NAT] means ($1-BitMajorityOutput(x,y))`1 = <*> &
  ($1-BitMajorityOutput(x,y))`2 = (0-tuples_on BOOLEAN)-->FALSE &
  proj1 ($1-BitMajorityOutput(x,y))`2 = 0-tuples_on BOOLEAN or
  card ($1-BitMajorityOutput(x,y))`1 = 3 &
  ($1-BitMajorityOutput(x,y))`2 = or3 &
  proj1 ($1-BitMajorityOutput(x,y))`2 = 3-tuples_on BOOLEAN;
A1: dom ((0-tuples_on BOOLEAN)-->FALSE) = 0-tuples_on BOOLEAN by FUNCOP_1:13;
  0-BitMajorityOutput(x,y) = [<*>, (0-tuples_on BOOLEAN)-->FALSE] by Th7;
  then
A2: P[ 0 ] by A1,MCART_1:7;
A3: now
    let n be Element of NAT;
    assume P[n];
    set c = n-BitMajorityOutput(x, y);
A4: (n+1)-BitMajorityOutput(x, y) =
    MajorityOutput(x .(n+1), y.(n+1), c) by Th12
      .= [<*[<*x .(n+1),y.(n+1)*>, '&'], [<*y.(n+1),c*>, '&'],
    [<*c,x .(n+1)*>, '&']*>, or3];
A5: dom or3 = 3-tuples_on BOOLEAN by FUNCT_2:def 1;
    ((n+1)-BitMajorityOutput(x, y))`1 = <*[<*x .(n+1),y.(n+1)*>, '&'], [<*y.
    (n+1),c*>, '&'], [<*c,x .(n+1)*>, '&']*> by A4,MCART_1:7;
    hence P[n+1] by A4,A5,FINSEQ_1:45,MCART_1:7;
  end;
  thus for n being Element of NAT holds P[n] from NAT_1:sch 1(A2,A3);
end;

theorem Th25:
  for n being Element of NAT, x,y being FinSequence, p being set holds
  n-BitMajorityOutput(x,y) <> [p, '&'] &
  n-BitMajorityOutput(x,y) <> [p, 'xor']
proof
  let n be Element of NAT, x,y be FinSequence, p be set;
A1: dom '&' = 2-tuples_on BOOLEAN by FUNCT_2:def 1;
A2: dom 'xor' = 2-tuples_on BOOLEAN by FUNCT_2:def 1;
A3: proj1 [p, '&']`2 = 2-tuples_on BOOLEAN by A1;
A4: proj1 [p, 'xor']`2 = 2-tuples_on BOOLEAN by A2;
  proj1 (n-BitMajorityOutput(x,y))`2 = 0-tuples_on BOOLEAN or
  proj1 (n-BitMajorityOutput(x,y))`2 = 3-tuples_on BOOLEAN by Th24;
  hence thesis by A3,A4,FINSEQ_2:110;
end;

theorem Th26:
  for f,g being nonpair-yielding FinSequence for n being Element of NAT holds
  InputVertices ((n+1)-BitAdderStr(f,g)) =
  (InputVertices (n-BitAdderStr(f,g)))\/
  ((InputVertices BitAdderWithOverflowStr(f.(n+1),g.(n+1),
  n-BitMajorityOutput(f,g)) \ {n-BitMajorityOutput(f,g)})) &
  InnerVertices (n-BitAdderStr(f,g)) is Relation &
  InputVertices (n-BitAdderStr(f,g)) is without_pairs
proof
  let f,g be nonpair-yielding FinSequence;
  deffunc Sn(Nat) = $1-BitAdderStr(f,g);
  deffunc S(set, Nat)
  = BitAdderWithOverflowStr(f.($2+1),g.($2+1), $1);
  deffunc H(Nat) = $1-BitMajorityOutput(f,g);
  consider h being ManySortedSet of NAT such that
A1: for n being Element of NAT holds h.n = H(n) from PBOOLE:sch 5;
  deffunc h(Nat) = h.$1;
  deffunc o(set, Nat) = MajorityOutput(f.($2+1),g.($2+1), $1);
  set k = (0-tuples_on BOOLEAN)-->FALSE;
A2: 0-BitAdderStr(f,g) = 1GateCircStr(<*>, k) by Th7;
  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-BitMajorityOutput(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 FACIRC_1:88;
A7: now
    let n be Nat, x be set such that
A8: x = h(n);
A9: n in NAT by ORDINAL1:def 12;
    then
A10: h(n) = n-BitMajorityOutput(f,g) by A1;
    then
A11: x <> [<*f.(n+1),g.(n+1)*>, '&'] by A8,A9,Th25;
    x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A8,A9,A10,Th25;
    hence InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A11,Th22;
  end;
A12: 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;
    assume x = h(n);
    then
A13: InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A7;
    thus (InputVertices S(x, n)) \ {x} is without_pairs
    proof
      let a be pair set;
      assume
A14:  a in (InputVertices S(x, n)) \ {x};
      then a in InputVertices S(x, n) by XBOOLE_0:def 5;
      then
A15:  a = f.(n+1) or a = g.(n+1) or a = x by A13,ENUMSET1:def 1;
      not a in {x} by A14,XBOOLE_0:def 5;
      hence contradiction by A15,TARSKI:def 1;
    end;
  end;
A16: now
    let n be Nat, S be non empty ManySortedSign, x be set;
A17: n in NAT by ORDINAL1:def 12;
    assume that
A18: S = Sn(n) and
A19: x = h.n;
A20: x = n-BitMajorityOutput(f,g) by A1,A17,A19;
A21: h(n+1) = (n+1)-BitMajorityOutput(f,g ) by A1;
    thus Sn(n+1) = S +* S(x,n) by A17,A18,A20,Th12;
    thus h.(n+1) = o(x, n) by A17,A20,A21,Th12;
    InputVertices S(x, n) = {f.(n+1), g.(n+1), x} by A7,A19;
    hence x in InputVertices S(x,n) by ENUMSET1:def 1;
A22: InnerVertices S(x, n) =
    {[<*f.(n+1),g.(n+1)*>, 'xor'], 2GatesCircOutput(f.(n+1),g.(n+1),x,'xor')}
    \/ {[<*f.(n+1),g.(n+1)*>,'&'], [<*g.(n+1),x*>,'&'],
    [<*x,f.(n+1)*>,'&']} \/ {MajorityOutput(f.(n+1),g.(n+1),x)} by Th23;
    o(x,n) in {o(x,n)} by TARSKI:def 1;
    hence o(x, n) in InnerVertices S(x, n) by A22,XBOOLE_0:def 3;
  end;
A23: 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
  ,A12,
  A16);
  let n be Element of NAT;
  h.n = n-BitMajorityOutput(f,g) by A1;
  hence thesis by A23;
end;

theorem
  for n being Element of NAT
  for x,y being nonpair-yielding FinSeqLen of n holds
  InputVertices (n-BitAdderStr(x,y)) = rng x \/ rng y
proof
  defpred P[Element of NAT] means
  for x,y being nonpair-yielding FinSeqLen of $1 holds
  InputVertices ($1-BitAdderStr(x,y)) = rng x \/ rng y;
A1: P[ 0 ]
  proof
    let x,y be nonpair-yielding FinSeqLen of 0;
    set f = (0-tuples_on BOOLEAN)-->FALSE;
    0-BitAdderStr(x,y) = 1GateCircStr(<*>, f) by Th7;
    hence thesis by CIRCCOMB:42;
  end;
A2: for i being Element of NAT st P[i] holds P[i+1]
  proof
    let i be Element of NAT such that
A3: P[i];
    let x,y be nonpair-yielding FinSeqLen of i+1;
    consider x9 being nonpair-yielding FinSeqLen of i,
    z1 being non pair set such that
A4: x = x9^<*z1*> by Lm2;
    consider y9 being nonpair-yielding FinSeqLen of i,
    z2 being non pair set such that
A5: y = y9^<*z2*> by Lm2;
    set S = (i+1)-BitAdderStr(x, y);
A6: 1 in Seg 1 by FINSEQ_1:1;
A7: dom <*z1*> = Seg 1 by FINSEQ_1:def 8;
A8: <*z1*>.1 = z1 by FINSEQ_1:def 8;
    len x9 = i by CARD_1:def 7;
    then
A9: x .(i+1) = z1 by A4,A6,A7,A8,FINSEQ_1:def 7;
A10: dom <*z2*> = Seg 1 by FINSEQ_1:def 8;
A11: <*z2*>.1 = z2 by FINSEQ_1:def 8;
    len y9 = i by CARD_1:def 7;
    then
A12: y .(i+1) = z2 by A5,A6,A10,A11,FINSEQ_1:def 7;
A13: {z1,z2,i-BitMajorityOutput(x,y)} = {i-BitMajorityOutput(x,y),z1,z2}
    by ENUMSET1:59;
A14: rng x = rng x9 \/ rng <*z1*> by A4,FINSEQ_1:31
      .= rng x9 \/ {z1} by FINSEQ_1:38;
A15: rng y = rng y9 \/ rng <*z2*> by A5,FINSEQ_1:31
      .= rng y9 \/ {z2} by FINSEQ_1:38;
A16: i-BitMajorityOutput(x,y) <> [<*z1,z2*>, '&'] by Th25;
A17: i-BitMajorityOutput(x,y) <> [<*z1,z2*>, 'xor'] by Th25;
A18: x9 = x9^{} by FINSEQ_1:34;
    y9 = y9^{} by FINSEQ_1:34;
    then i-BitAdderStr(x,y) = i-BitAdderStr(x9,y9) by A4,A5,A18,Th10;
    hence InputVertices S = (InputVertices (i-BitAdderStr(x9,y9)))\/
    ((InputVertices BitAdderWithOverflowStr(z1,z2,
    i-BitMajorityOutput(x,y)) \ {i-BitMajorityOutput(x,y)})) by A9,A12,Th26
      .= (rng x9 \/ rng y9)\/ ((InputVertices BitAdderWithOverflowStr(z1,z2,
    i-BitMajorityOutput(x,y)) \ {i-BitMajorityOutput(x,y)})) by A3
      .= (rng x9 \/ rng y9)\/
    ({z1,z2,i-BitMajorityOutput(x,y)} \ {i-BitMajorityOutput(x,y)})
    by A16,A17,Th22
      .= (rng x9 \/ rng y9)\/ {z1,z2} by A13,ENUMSET1:86
      .= rng x9 \/ rng y9 \/ ({z1} \/ {z2}) by ENUMSET1:1
      .= rng x9 \/ rng y9 \/ {z1} \/ {z2} by XBOOLE_1:4
      .= rng x9 \/ {z1} \/ rng y9 \/ {z2} by XBOOLE_1:4
      .= rng x \/ rng y by A14,A15,XBOOLE_1:4;
  end;
  thus for i being Element of NAT holds P[i] from NAT_1:sch 1(A1,A2);
end;

Lm3: for x,y,c being set for s being State of MajorityCirc(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*>,'&'] = a1 '&' a2 &
(Following s).[<*y,c*>,'&'] = a2 '&' a3 &
(Following s).[<*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be set;
  let s be State of MajorityCirc(x,y,c);
  let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
  set S = MajorityStr(x,y,c);
A4: InnerVertices S = the carrier' of S by FACIRC_1:37;
A5: dom s = the carrier of S by CIRCUIT1:3;
A6: x in the carrier of S by FACIRC_1:72;
A7: y in the carrier of S by FACIRC_1:72;
A8: c in the carrier of S by FACIRC_1:72;
  [<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) by FACIRC_1:73;
  hence (Following s).[<*x,y*>,'&'] = '&'.(s*<*x,y*>) by A4,FACIRC_1:35
    .= '&'.<*a1,a2*> by A1,A2,A5,A6,A7,FINSEQ_2:125
    .= a1 '&' a2 by FACIRC_1:def 6;
  [<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) by FACIRC_1:73;
  hence (Following s).[<*y,c*>,'&'] = '&'.(s*<*y,c*>) by A4,FACIRC_1:35
    .= '&'.<*a2,a3*> by A2,A3,A5,A7,A8,FINSEQ_2:125
    .= a2 '&' a3 by FACIRC_1:def 6;
  [<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c) by FACIRC_1:73;
  hence (Following s).[<*c,x*>,'&'] = '&'.(s*<*c,x*>) by A4,FACIRC_1:35
    .= '&'.<*a3,a1*> by A1,A3,A5,A6,A8,FINSEQ_2:125
    .= a3 '&' a1 by FACIRC_1:def 6;
end;

theorem Th28:
  for x,y,c being set for s being State of MajorityCirc(x,y,c)
  for a1,a2,a3 being Element of BOOLEAN st
  a1 = s.[<*x,y*>,'&'] & a2 = s.[<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&']
  holds (Following s).MajorityOutput(x,y,c) = a1 'or' a2 'or' a3
proof
  let x,y,c be set;
  let s be State of MajorityCirc(x,y,c);
  let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.[<*x,y*>,'&'] and
A2: a2 = s.[<*y,c*>,'&'] and
A3: a3 = s.[<*c,x*>,'&'];
  set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
  set S = MajorityStr(x,y,c);
A4: InnerVertices S = the carrier' of S by FACIRC_1:37;
A5: dom s = the carrier of S by CIRCUIT1:3;
  reconsider xy, yc, cx as Element of InnerVertices S by FACIRC_1:73;
  thus (Following s).MajorityOutput(x,y,c)
  = or3.(s*<*xy, yc, cx*>) by A4,FACIRC_1:35
    .= or3.<*a1,a2,a3*> by A1,A2,A3,A5,FINSEQ_2:126
    .= a1 'or' a2 'or' a3 by FACIRC_1:def 7;
end;

Lm4: for x,y,c being set st
x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&']
for s being State of MajorityCirc(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)).MajorityOutput(x,y,c) =
a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 &
(Following(s,2)).[<*x,y*>,'&'] = a1 '&' a2 &
(Following(s,2)).[<*y,c*>,'&'] = a2 '&' a3 &
(Following(s,2)).[<*c,x*>,'&'] = a3 '&' a1
proof
  let x,y,c be set such that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'];
  let s be State of MajorityCirc(x,y,c);
  let a1,a2,a3 be Element of BOOLEAN such that
A4: a1 = s.x and
A5: a2 = s.y and
A6: a3 = s.c;
  set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
  set S = MajorityStr(x,y,c);
  reconsider x9 = x, y9 = y, c9 = c as Vertex of S by FACIRC_1:72;
A7: InputVertices S = {x,y,c} by A1,A2,A3,Th20;
  then
A8: x in InputVertices S by ENUMSET1:def 1;
A9: y in InputVertices S by A7,ENUMSET1:def 1;
A10: c in InputVertices S by A7,ENUMSET1:def 1;
A11: (Following s).x9 = s.x by A8,CIRCUIT2:def 5;
A12: (Following s).y9 = s.y by A9,CIRCUIT2:def 5;
A13: (Following s).c9 = s.c by A10,CIRCUIT2:def 5;
A14: Following(s,2) = Following Following s by FACIRC_1:15;
A15: (Following s).xy = a1 '&' a2 by A4,A5,A6,Lm3;
A16: (Following s).yc = a2 '&' a3 by A4,A5,A6,Lm3;
  (Following s).cx = a3 '&' a1 by A4,A5,A6,Lm3;
  hence (Following(s,2)).MajorityOutput(x,y,c) =
  a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by A14,A15,A16,Th28;
  thus thesis by A4,A5,A6,A11,A12,A13,A14,Lm3;
end;

theorem Th29:
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&']
  for s being State of MajorityCirc(x,y,c)
  holds Following(s,2) is stable
proof
  let x,y,c be set;
  set S = MajorityStr(x,y,c);
  assume that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'];
  let s be State of MajorityCirc(x,y,c);
A4: dom Following Following(s,2) = the carrier of S by CIRCUIT1:3;
A5: dom Following(s,2) = the carrier of S by CIRCUIT1:3;
  reconsider xx = x, yy = y, cc = c as Vertex of S by FACIRC_1:72;
  set a1 = s.xx, a2 = s.yy, a3 = s.cc;
  set ffs = Following(s,2), fffs = Following ffs;
A6: a1 = s.x;
A7: a2 = s.y;
A8: a3 = s.c;
A9: ffs.MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by A1
,A2,A3,Lm4;
A10: ffs.[<*x,y*>,'&'] = a1 '&' a2 by A1,A2,A3,A8,Lm4;
A11: ffs.[<*y,c*>,'&'] = a2 '&' a3 by A1,A2,A3,A6,Lm4;
A12: ffs.[<*c,x*>,'&'] = a3 '&' a1 by A1,A2,A3,A7,Lm4;
A13: ffs = Following Following s by FACIRC_1:15;
A14: InputVertices S = {x,y,c} by A1,A2,A3,Th20;
  then
A15: x in InputVertices S by ENUMSET1:def 1;
A16: y in InputVertices S by A14,ENUMSET1:def 1;
A17: c in InputVertices S by A14,ENUMSET1:def 1;
A18: (Following s).x = a1 by A15,CIRCUIT2:def 5;
A19: (Following s).y = a2 by A16,CIRCUIT2:def 5;
A20: (Following s).c = a3 by A17,CIRCUIT2:def 5;
A21: ffs.x = a1 by A13,A15,A18,CIRCUIT2:def 5;
A22: ffs.y = a2 by A13,A16,A19,CIRCUIT2:def 5;
A23: ffs.c = a3 by A13,A17,A20,CIRCUIT2:def 5;
  now
    let a be set;
    assume
A24: a in the carrier of S;
    then reconsider v = a as Vertex of S;
A25: v in InputVertices S \/ InnerVertices S by A24,XBOOLE_1:45;
    thus ffs.a = (fffs).a proof per cases by A25,XBOOLE_0:def 3;
      suppose v in InputVertices S;
        hence thesis by CIRCUIT2:def 5;
      end;
      suppose v in InnerVertices S;
        then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
        {MajorityOutput(x,y,c)} by Th19;
        then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} or
        v in {MajorityOutput(x,y,c)} by XBOOLE_0:def 3;
        then v = [<*x,y*>,'&'] or v = [<*y,c*>,'&'] or v = [<*c,x*>,'&'] or
        v = MajorityOutput(x,y,c) by ENUMSET1:def 1,TARSKI:def 1;
        hence thesis by A9,A10,A11,A12,A21,A22,A23,Lm3,Th28;
      end;
    end;
  end;
  hence ffs = fffs by A4,A5,FUNCT_1:2;
end;

theorem
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&'] &
  c <> [<*x,y*>, 'xor'] for s being State of BitAdderWithOverflowCirc(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)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3 &
  (Following(s,2)).MajorityOutput(x,y,c)
  = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1
proof
  let x,y,c be set such that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'] and
A4: c <> [<*x,y*>, 'xor'];
  set f = 'xor';
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
  set A = BitAdderWithOverflowCirc(x,y,c);
  set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
  let s be State of A;
  let a1,a2,a3 be Element of BOOLEAN;
  assume that
A5: a1 = s.x and
A6: a2 = s.y and
A7: a3 = s.c;
A8: x in the carrier of S1 by FACIRC_1:60;
A9: y in the carrier of S1 by FACIRC_1:60;
A10: c in the carrier of S1 by FACIRC_1:60;
A11: x in the carrier of S2 by FACIRC_1:72;
A12: y in the carrier of S2 by FACIRC_1:72;
A13: c in the carrier of S2 by FACIRC_1:72;
  reconsider s1 = s|the carrier of S1 as State of A1 by FACIRC_1:26;
  reconsider s2 = s|the carrier of S2 as State of A2 by FACIRC_1:26;
  reconsider t = s as State of A1+*A2;
  InputVertices S1 = {x,y,c} by A4,FACIRC_1:57;
  then
A14: InputVertices S1 = InputVertices S2 by A1,A2,A3,Th20;
A15: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A16: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
A17: dom s1 = the carrier of S1 by CIRCUIT1:3;
  then
A18: a1 = s1.x by A5,A8,FUNCT_1:47;
A19: a2 = s1.y by A6,A9,A17,FUNCT_1:47;
A20: a3 = s1.c by A7,A10,A17,FUNCT_1:47;
  (Following(t,2)).2GatesCircOutput(x,y,c, f) = (Following(s1,2)).
  2GatesCircOutput(x,y,c, f) by A14,A16,FACIRC_1:32;
  hence (Following(s,2)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3
  by A4,A18,A19,A20,FACIRC_1:64;
A21: dom s2 = the carrier of S2 by CIRCUIT1:3;
  then
A22: a1 = s2.x by A5,A11,FUNCT_1:47;
A23: a2 = s2.y by A6,A12,A21,FUNCT_1:47;
A24: a3 = s2.c by A7,A13,A21,FUNCT_1:47;
  (Following(t,2)).MajorityOutput(x,y,c) = (Following(s2,2)).
  MajorityOutput(x,y,c) by A14,A15,FACIRC_1:33;
  hence thesis by A1,A2,A3,A22,A23,A24,Lm4;
end;

theorem Th31:
  for x,y,c being set st
  x <> [<*y,c*>, '&'] & y <> [<*c,x*>, '&'] & c <> [<*x,y*>, '&'] &
  c <> [<*x,y*>, 'xor'] for s being State of BitAdderWithOverflowCirc(x,y,c)
  holds Following(s,2) is stable
proof
  let x,y,c be set such that
A1: x <> [<*y,c*>, '&'] and
A2: y <> [<*c,x*>, '&'] and
A3: c <> [<*x,y*>, '&'] and
A4: c <> [<*x,y*>, 'xor'];
  set S = BitAdderWithOverflowStr(x,y,c);
  set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
  set A = BitAdderWithOverflowCirc(x,y,c);
  set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
  let s be State of A;
  reconsider s1 = s|the carrier of S1 as State of A1 by FACIRC_1:26;
  reconsider s2 = s|the carrier of S2 as State of A2 by FACIRC_1:26;
  reconsider t = s as State of A1+*A2;
  InputVertices S1 = {x,y,c} by A4,FACIRC_1:57;
  then
A5: InputVertices S1 = InputVertices S2 by A1,A2,A3,Th20;
A6: InnerVertices S1 misses InputVertices S1 by XBOOLE_1:79;
A7: InnerVertices S2 misses InputVertices S2 by XBOOLE_1:79;
  then
A8: Following(s1,2) = Following(t,2)|the carrier of S1 by A5,FACIRC_1:30;
A9: Following(s1,3) = Following(t,3)|the carrier of S1 by A5,A7,FACIRC_1:30;
A10: Following(s2,2) = Following(t,2)|the carrier of S2 by A5,A6,FACIRC_1:31;
A11: Following(s2,3) = Following(t,3)|the carrier of S2 by A5,A6,FACIRC_1:31;
  Following(s1,2) is stable by A4,FACIRC_1:63;
  then
A12: Following(s1,2) = Following Following(s1,2) by CIRCUIT2:def 6
    .= Following(s1,2+1) by FACIRC_1:12;
  Following(s2,2) is stable by A1,A2,A3,Th29;
  then
A13: Following(s2,2) = Following Following(s2,2) by CIRCUIT2:def 6
    .= Following(s2,2+1) by FACIRC_1:12;
A14: Following(s,2+1) = Following Following(s,2) by FACIRC_1:12;
A15: dom Following(s,2) = the carrier of S by CIRCUIT1:3;
A16: dom Following(s,3) = the carrier of S by CIRCUIT1:3;
A17: dom Following(s1,2) = the carrier of S1 by CIRCUIT1:3;
A18: dom Following(s2,2) = the carrier of S2 by CIRCUIT1:3;
A19: the carrier of S = (the carrier of S1) \/ the carrier of S2
  by CIRCCOMB:def 2;
  now
    let a be set;
    assume a in the carrier of S;
    then a in the carrier of S1 or a in the carrier of S2 by A19,XBOOLE_0:def 3
;
    then (Following(s,2)).a = (Following(s1,2)).a &
    (Following(s,3)).a = (Following(s1,3)).a or
    (Following(s,2)).a = (Following(s2,2)).a &
    (Following(s,3)).a = (Following(s2,3)).a by A8,A9,A10,A11,A12,A13,A17,A18,
FUNCT_1:47;
    hence (Following(s,2)).a = (Following Following(s,2)).a by A12,A13,
FACIRC_1:12;
  end;
  hence Following(s,2) = Following Following(s,2) by A14,A15,A16,FUNCT_1:2;
end;

Lm5: for n being Element of NAT
ex N being Function of NAT,NAT st N.0 = 1 & N.1 = 2 & N.2 = n
proof
  let n be Element of NAT;
  defpred P[set] means $1 = 0;
  deffunc F(set) = 1;
  deffunc G(set) = 2;
  consider N0 being Function such that dom N0 = NAT and
A1: for i be set st i in NAT holds
  (P[i] implies N0.i = F(i)) & (not P[i] implies N0.i = G(i)) from
  PARTFUN1:sch 1;
  defpred P[set] means $1 <> 2;
  deffunc F(set) = N0.$1;
  deffunc G(set) = n;
  consider N being Function such that
A2: dom N = NAT and
A3: for i be set st i in NAT holds
  (P[i] implies N.i = F(i)) & (not P[i] implies N.i = G(i)) from
  PARTFUN1:sch 1;
  rng N c= NAT
  proof
    let x be set;
    assume x in rng N;
    then consider i being set such that
A4: i in dom N and
A5: x = N.i by FUNCT_1:def 3;
    reconsider i as Element of NAT by A2,A4;
    x = n or x = N0.i & (i = 0 or i <> 0) by A3,A5;
    then x = n or x = 1 or x = 2 by A1;
    hence thesis;
  end;
  then reconsider N as Function of NAT,NAT by A2,FUNCT_2:2;
  take N;
A6: N.0 = N0.0 by A3;
  N0.1 = N.1 by A3;
  hence N.0 = 1 & N.1 = 2 by A1,A6;
  thus thesis by A3;
end;

theorem
  for n being Element of NAT for x,y being nonpair-yielding FinSeqLen of n
  for s being State of n-BitAdderCirc(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)
  = BitAdderWithOverflowStr(f.($2+1), g.($2+1), $1);
  deffunc A(set,Nat)
  = BitAdderWithOverflowCirc(f.($2+1), g.($2+1), $1);
  deffunc o(set,Nat) = MajorityOutput(f.($2+1), g.($2+1), $1);
  set S0 = 1GateCircStr(<*>, (0-tuples_on BOOLEAN)-->FALSE);
  set A0 = 1GateCircuit(<*>, (0-tuples_on BOOLEAN)-->FALSE);
  consider N being Function of NAT,NAT such that
A1: N.0 = 1 and
A2: N.1 = 2 and
A3: N.2 = n by Lm5;
  deffunc n(Element of NAT) = N.$1;
A4: for x being set, n being Nat holds
  A(x,n) is Boolean gate`2=den strict Circuit of S(x,n);
A5: now
    let s be State of A0;
    Following(s, 1) = Following s by FACIRC_1:14;
    hence Following(s, n(0)) is stable by A1,CIRCCMB2:2;
  end;
  deffunc F(Element of NAT) = $1-BitMajorityOutput(f,g);
  consider h being ManySortedSet of NAT such that
A6: for n being Element of NAT holds h.n = F(n) from PBOOLE:sch 5;
A7: 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);
A8: n in NAT by ORDINAL1:def 12;
    assume x = h.n;
    then
A9: x = n-BitMajorityOutput(f,g) by A6,A8;
    then
A10: x <> [<*f.(n+1),g.(n+1)*>, '&'] by A8,Th25;
    x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A8,A9,Th25;
    hence thesis by A2,A10,Th31;
  end;
  set Sn = n-BitAdderStr(f,g);
  set An = n-BitAdderCirc(f,g);
  set o0 = 0-BitMajorityOutput(f,g);
  consider f1,g1,h1 being ManySortedSet of NAT such that
A11: n-BitAdderStr(f,g) = f1.n and
A12: n-BitAdderCirc(f,g) = g1.n and
A13: f1.0 = 1GateCircStr(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A14: g1.0 = 1GateCircuit(<*>,(0-tuples_on BOOLEAN)-->FALSE) and
A15: h1.0 = [<*>, (0-tuples_on BOOLEAN)-->FALSE] and
A16: for n 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 +* BitAdderWithOverflowStr(f.(n+1), g.(n+1), z) & g1.(n+1) =
A +* BitAdderWithOverflowCirc(f.(n+1), g.(n+1), z) & h1.(n+1) = MajorityOutput(
  f.(n+1), g.(n+1), z)
  by Def4;
  now
    let i be set;
    assume i in NAT;
    then reconsider j = i as Element of NAT;
    thus h1.i = j-BitMajorityOutput(f,g) by A13,A14,A15,A16,Th6
      .= h.i by A6;
  end;
  then
A17: h1 = h by PBOOLE:3;
A18: ex u,v 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 A3,A6,A11,A12,A13,A14,A16,A17;
  end;
A19: InnerVertices S0 is Relation & InputVertices S0 is without_pairs
  by FACIRC_1:38,39;
A20: [<*>, (0-tuples_on BOOLEAN)-->FALSE] = o0 by Th7;
  InnerVertices S0 = {[<*>, (0-tuples_on BOOLEAN)-->FALSE]} by CIRCCOMB:42;
  then
A21: h.0 = o0 & o0 in InnerVertices S0 by A6,A20,TARSKI:def 1;
A22: for n being Nat, x being set
  holds InnerVertices S(x,n) is Relation by FACIRC_1:88;
A23: 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
A24: x = h.n;
A25: n in NAT by ORDINAL1:def 12;
    then
A26: x = n-BitMajorityOutput(f,g) by A6,A24;
    then
A27: x <> [<*f.(n+1),g.(n+1)*>, '&'] by A25,Th25;
    x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A25,A26,Th25;
    then
A28: InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by A27,Th22;
    let a be pair set;
    assume
A29: a in (InputVertices S(x, n)) \ {x};
    then
A30: a in {f.(n+1),g.(n+1),x} by A28,XBOOLE_0:def 5;
A31: not a in {x} by A29,XBOOLE_0:def 5;
    a = f.(n+1) or a = g.(n+1) or a = x by A30,ENUMSET1:def 1;
    hence thesis by A31,TARSKI:def 1;
  end;
A32: 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
A33: x = h.n;
A34: n in NAT by ORDINAL1:def 12;
    then
A35: x = n-BitMajorityOutput(f,g) by A6,A33;
    h.(n+1) = (n+1)-BitMajorityOutput(f,g) by A6;
    hence h.(n+1) = o(x, n) by A34,A35,Th12;
A36: x <> [<*f.(n+1),g.(n+1)*>, '&'] by A34,A35,Th25;
    x <> [<*f.(n+1),g.(n+1)*>, 'xor'] by A34,A35,Th25;
    then InputVertices S(x, n) = {f.(n+1),g.(n+1),x} by A36,Th22;
    hence x in InputVertices S(x, n) by ENUMSET1:def 1;
    set xx = f.(n+1), xy = g.(n+1);
A37: o(x, n) in {o(x, n)} by TARSKI:def 1;
    InnerVertices S(x, n) =
    {[<*xx,xy*>, 'xor'], 2GatesCircOutput(xx,xy,x,'xor')} \/
    {[<*xx,xy*>,'&'], [<*xy,x*>,'&'], [<*x,xx*>,'&']} \/
    {MajorityOutput(xx,xy,x)} by Th23;
    hence thesis by A37,XBOOLE_0:def 3;
  end;
  for s being State of An holds Following(s,n(0)+n(2)*n(1)) is stable
  from CIRCCMB2:sch 22(A4,A5,A7,A18,A19,A21,A22,A23,A32);
  hence thesis by A1,A2,A3;
end;

theorem
  for i being Element of NAT, x being FinSeqLen of i+1
  ex y being FinSeqLen of i, a being set st x = y^<*a*> by Lm1;

theorem
  for i being Element of NAT, x being nonpair-yielding FinSeqLen of i+1
  ex y being nonpair-yielding FinSeqLen of i,
  a being non pair set st x = y^<*a*> by Lm2;

theorem
  for n being Element of NAT
  ex N being Function of NAT,NAT st N.0 = 1 & N.1 = 2 & N.2 = n by Lm5;