:: FACIRC_2 semantic presentation

begin

theorem Th1: :: FACIRC_2:1
for x, y, z being set st x <> z & y <> z holds
{x,y} \ {z} = {x,y}
proof
let x, y, z be set ; ::_thesis: ( x <> z & y <> z implies {x,y} \ {z} = {x,y} )
assume that
A1: x <> z and
A2: y <> z ; ::_thesis: {x,y} \ {z} = {x,y}
 for a being set st a in {x,y} holds
not a in {z}
proof
let a be set ; ::_thesis: ( a in {x,y} implies not a in {z} )
assume  a in {x,y} ; ::_thesis: not a in {z}
then  a <> z by A1, A2, TARSKI:def_2;
hence  not a in {z} by TARSKI:def_1; ::_thesis: verum
end;
then  {x,y} misses {z} by XBOOLE_0:3;
hence  {x,y} \ {z} = {x,y} by XBOOLE_1:83; ::_thesis: verum
end;

theorem :: FACIRC_2:2
for x, y, z being set holds
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
proof
let x, y, z be set ; ::_thesis: ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
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  ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] ) by A4; ::_thesis: verum
end;

registration
cluster void  ->  unsplit gate`1=arity gate`2isBoolean for ManySortedSign ;
coherence
 for b1 being ManySortedSign st b1 is void holds
( b1 is unsplit & b1 is gate`1=arity & b1 is gate`2isBoolean )
proof
let S be ManySortedSign ; ::_thesis: ( S is void implies ( S is unsplit & S is gate`1=arity & S is gate`2isBoolean ) )
assume A1: the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: ( S is unsplit & S is gate`1=arity & S is gate`2isBoolean )
hence  the ResultSort of S = {}
.= id the carrier' of S by A1 ;
:: according to CIRCCOMB:def_7 ::_thesis: ( S is gate`1=arity & S is gate`2isBoolean )
thus  S is gate`1=arity ::_thesis: S is gate`2isBoolean
proof
let g be set ; :: according to CIRCCOMB:def_8 ::_thesis: ( not g in the carrier' of S or g = [( the Arity of S . g),(g `2)] )
thus  ( not g in the carrier' of S or g = [( the Arity of S . g),(g `2)] ) by A1; ::_thesis: verum
end;
let g be set ; :: according to CIRCCOMB:def_9 ::_thesis: ( not g in the carrier' of S or for b1 being set holds
( not b1 = the Arity of S . g or ex b2 being Element of K23(K24(((len b1) -tuples_on BOOLEAN),BOOLEAN)) st g = [(g `1),b2] ) )
thus  ( not g in the carrier' of S or for b1 being set holds
( not b1 = the Arity of S . g or ex b2 being Element of K23(K24(((len b1) -tuples_on BOOLEAN),BOOLEAN)) st g = [(g `1),b2] ) ) by A1; ::_thesis: verum
end;
end;

registration
cluster void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is strict & b1 is void )
proof
set S = the void strict ManySortedSign ;
take  the void strict ManySortedSign ; ::_thesis: ( the void strict ManySortedSign is strict & the void strict ManySortedSign is void )
thus  ( the void strict ManySortedSign is strict & the void strict ManySortedSign is void ) ; ::_thesis: verum
end;
end;

definition
let x be set ;
func SingleMSS x ->  void strict ManySortedSign  means :Def1: :: FACIRC_2:def 1
 the carrier of it = {x};
existence
 ex b1 being void strict ManySortedSign st the carrier of b1 = {x}
proof
set a = the Function of {},({x} *);
set r = the Function of {},{x};
reconsider S = ManySortedSign(# {x},{}, the Function of {},({x} *), the Function of {},{x} #) as void strict ManySortedSign ;
take  S ; ::_thesis: the carrier of S = {x}
thus  the carrier of S = {x} ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being void strict ManySortedSign st the carrier of b1 = {x} & the carrier of b2 = {x} holds
b1 = b2
proof
let S1, S2 be void strict ManySortedSign ; ::_thesis: ( the carrier of S1 = {x} & the carrier of S2 = {x} implies S1 = S2 )
assume that
A1: the carrier of S1 = {x} and
A2: the carrier of S2 = {x} ; ::_thesis: S1 = S2
 the Arity of S1 = the Arity of S2 ;
hence  S1 = S2 by A1, A2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines SingleMSS FACIRC_2:def_1_:_
 for x being set
for b2 being void strict ManySortedSign holds
( b2 = SingleMSS x iff the carrier of b2 = {x} );

registration
let x be set ;
cluster SingleMSS x ->  non empty void strict ;
coherence
 not SingleMSS x is empty
proof
 the carrier of (SingleMSS x) = {x} by Def1;
hence  not the carrier of (SingleMSS x) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let x be set ;
func SingleMSA x ->  strict Boolean MSAlgebra over SingleMSS x means :: FACIRC_2:def 2
verum;
existence
 ex b1 being strict Boolean MSAlgebra over SingleMSS x st verum ;
uniqueness
 for b1, b2 being strict Boolean MSAlgebra over SingleMSS x holds b1 = b2
proof
set S = SingleMSS x;
let A1, A2 be strict Boolean MSAlgebra over SingleMSS x; ::_thesis: A1 = A2
A1: the Sorts of A1 = the carrier of (SingleMSS x) --> BOOLEAN by CIRCCOMB:57;
A2: the Charact of A1 = {} ;
 the Charact of A2 = {} ;
hence  A1 = A2 by A1, A2, CIRCCOMB:57; ::_thesis: verum
end;
end;

:: deftheorem  defines SingleMSA FACIRC_2:def_2_:_
 for x being set
for b2 being strict Boolean MSAlgebra over SingleMSS x holds
( b2 = SingleMSA x iff verum );

theorem :: FACIRC_2:3
for x being set
for S being ManySortedSign holds SingleMSS x tolerates S
proof
let x be set ; ::_thesis: for S being ManySortedSign holds SingleMSS x tolerates S
let S be ManySortedSign ; ::_thesis: SingleMSS x tolerates S
thus  ( the Arity of (SingleMSS x) tolerates the Arity of S & the ResultSort of (SingleMSS x) tolerates the ResultSort of S ) by PARTFUN1:59; :: according to CIRCCOMB:def_1 ::_thesis: verum
end;

theorem Th4: :: FACIRC_2:4
for x being set
for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)
proof
let x be set ; ::_thesis: for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)
let S be non empty ManySortedSign ; ::_thesis: ( x in the carrier of S implies (SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) )
set T = (SingleMSS x) +* S;
assume  x in the carrier of S ; ::_thesis: (SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort 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 ((SingleMSS x) +* S) = the carrier of S by A1, A3, CIRCCOMB:def_2;
A9: the carrier' of ((SingleMSS x) +* S) = the carrier' of S by A2, A4, CIRCCOMB:def_2;
 the ResultSort of ((SingleMSS x) +* S) = the ResultSort of S by A4, A6, CIRCCOMB:def_2;
hence  (SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) by A5, A7, A8, A9, CIRCCOMB:def_2; ::_thesis: verum
end;

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

notation
synonym  <*> for  {} ;
end;

definition
let n be Nat;
let x, y be FinSequence;
A1: ( 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is unsplit & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is gate`1=arity & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is gate`2isBoolean & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is void & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is empty & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) is strict ) ;
funcn -BitAdderStr (x,y) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  means :Def3: :: FACIRC_2:def 3
 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
for S being non empty ManySortedSign
for z being 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
 for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) holds
b1 = b2
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
deffunc H1( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
 for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean 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
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & h . (n + 1) = H1(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
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H2(S,x,n) & h . (n + 1) = H1(x,n) ) ) ) holds
S1 = S2 from CIRCCMB2:sch_9();
hence  for b1, b2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
existence
 ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) )
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
deffunc H1( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( set , Nat) ->  ManySortedSign = BitAdderWithOverflowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1);
 ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex 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
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* H2(x,n) & h . (n + 1) = H1(x,n) ) ) ) from CIRCCMB2:sch_8(A1);
hence  ex b1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines -BitAdderStr FACIRC_2:def_3_:_
 for n being Nat
for x, y being FinSequence
for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitAdderStr (x,y) iff ex f, g being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being 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) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
funcn -BitAdderCirc (x,y) ->  strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) means :Def4: :: FACIRC_2:def 4
 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
for S being non empty ManySortedSign
for 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
 for b1, b2 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) st ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b1 = 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
for S being non empty ManySortedSign
for 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) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b2 = 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
for S being non empty ManySortedSign
for 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) ) ) ) holds
b1 = b2
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 H1( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H3( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) ->  MSAlgebra over $1 +* (BitAdderWithOverflowStr ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitAdderWithOverflowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3));
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
thus  for A1, A2 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) st ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & A1 = 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
for S being non empty ManySortedSign
for 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) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & A2 = 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
for S being non empty ManySortedSign
for 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) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) holds
A1 = A2 from CIRCCMB2:sch_21(A1); ::_thesis: verum
end;
existence
 ex b1 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b1 = 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
for S being non empty ManySortedSign
for 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) ) ) )
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 H1( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H3( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) ->  MSAlgebra over $1 +* (BitAdderWithOverflowStr ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitAdderWithOverflowCirc ((x . ($4 + 1)),(y . ($4 + 1)),$3));
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for z being set
for n being Nat holds
( H2(S,z,n) is unsplit & H2(S,z,n) is gate`1=arity & H2(S,z,n) is gate`2isBoolean & not H2(S,z,n) is void & H2(S,z,n) is strict ) ;
A3: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being strict gate`2=den Boolean Circuit of S
for z being set
for n being Nat st S1 = H2(S,z,n) holds
H3(S,A,z,n) is strict gate`2=den Boolean Circuit of S1 ;
A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
A5: ex f, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = H2(S,z,n) & h . (n + 1) = H1(z,n) ) ) ) by Def3;
thus  ex A being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & A = 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
for S being non empty ManySortedSign
for 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) = H2(S,x,n) & g . (n + 1) = H3(S,A,x,n) & h . (n + 1) = H1(x,n) ) ) ) from CIRCCMB2:sch_19(A2, A5, A4, A3); ::_thesis: verum
end;
end;

:: deftheorem Def4 defines -BitAdderCirc FACIRC_2:def_4_:_
 for n being Nat
for x, y being FinSequence
for b4 being strict gate`2=den Boolean Circuit of n -BitAdderStr (x,y) holds
( b4 = n -BitAdderCirc (x,y) iff ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b4 = 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
for S being non empty ManySortedSign
for 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) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
funcn -BitMajorityOutput (x,y) ->  Element of InnerVertices (n -BitAdderStr (x,y)) means :Def5: :: FACIRC_2:def 5
 ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) );
uniqueness
 for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) & ex h being ManySortedSet of NAT st
( b2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
b1 = b2
proof
let o1, o2 be Element of InnerVertices (n -BitAdderStr (x,y)); ::_thesis: ( ex h being ManySortedSet of NAT st
( o1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) & ex h being ManySortedSet of NAT st
( o2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) implies o1 = o2 )
given h1 being ManySortedSet of NAT  such that A1: o1 = h1 . n and
A2: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A3: for n being Nat
for z being set st z = h1 . n holds
h1 . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ; ::_thesis: ( for h being ManySortedSet of NAT holds
( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] or ex n being Nat ex z being set st
( z = h . n & not h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) or o1 = o2 )
given h2 being ManySortedSet of NAT  such that A4: o2 = h2 . n and
A5: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A6: for n being Nat
for z being set st z = h2 . n holds
h2 . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ; ::_thesis: o1 = o2
deffunc H1( Nat, set ) ->  Element of InnerVertices (MajorityStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = MajorityOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
A7: dom h1 = NAT by PARTFUN1:def_2;
A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A2;
A9: for n being Nat holds h1 . (n + 1) = H1(n,h1 . n) by A3;
A10: dom h2 = NAT by PARTFUN1:def_2;
A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A5;
A12: for n being Nat holds h2 . (n + 1) = H1(n,h2 . n) by A6;
 h1 = h2 from NAT_1:sch_15(A7, A8, A9, A10, A11, A12);
hence  o1 = o2 by A1, A4; ::_thesis: verum
end;
existence
 ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) )
proof
defpred S1[ set , set , set ] means verum;
deffunc H1( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H2( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = 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 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A16: for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = H1(S,z,n) & g . (n + 1) = H2(z,n) ) by Def3;
defpred S2[ 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))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42;
then  [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) by TARSKI:def_1;
then A17: S2[ 0 ] by A14, A15;
A18: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume 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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 for i being Element of NAT holds S2[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 ; ::_thesis: ex h being ManySortedSet of NAT st
( o = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) )
take  g ; ::_thesis: ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = g . n holds
g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) )
thus  ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] ) by A15; ::_thesis: for n being Nat
for z being set st z = g . n holds
g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z)
let i be Nat; ::_thesis: for z being set st z = g . i holds
g . (i + 1) = MajorityOutput ((x . (i + 1)),(y . (i + 1)),z)
A24: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = g . 0 & S1[S,x, 0 ] ) by A14;
A25: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = g . n & S1[S,x,n] holds
S1[H1(S,x,n),H2(x,n),n + 1] ;
 for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S1[S,g . n,n] ) from CIRCCMB2:sch_2(A24, A16, A25);
then  ex S being non empty ManySortedSign st S = f . i ;
hence  for z being set st z = g . i holds
g . (i + 1) = MajorityOutput ((x . (i + 1)),(y . (i + 1)),z) by A16; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def_5_:_
 for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b4 = n -BitMajorityOutput (x,y) iff ex h being ManySortedSet of NAT st
( b4 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );

theorem Th6: :: FACIRC_2:6
for x, y being FinSequence
for 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
for S being non empty ManySortedSign
for 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) ) ) holds
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; ::_thesis: for 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
for S being non empty ManySortedSign
for 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) ) ) holds
for n being Nat holds
( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n )
let f, g, h be ManySortedSet of NAT ; ::_thesis: ( 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
for S being non empty ManySortedSign
for 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) ) ) implies for n being Nat holds
( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n ) )
deffunc H1( set , Nat) ->  Element of InnerVertices (MajorityStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = MajorityOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( Nat, set ) ->  Element of InnerVertices (MajorityStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = MajorityOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
deffunc H3( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H4( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) ->  MSAlgebra over $1 +* (BitAdderWithOverflowStr ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $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
for S being non empty ManySortedSign
for 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) = H3(S,z,n) & g . (n + 1) = H4(S,A,z,n) & h . (n + 1) = H1(z,n) ) ; ::_thesis: for n being Nat holds
( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n )
let n be Nat; ::_thesis: ( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n )
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
for S being non empty ManySortedSign
for 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) = H3(S,z,n) & g1 . (n + 1) = H4(S,A,z,n) & h1 . (n + 1) = H1(z,n) ) by Def4;
A10: ex S being non empty ManySortedSign ex 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
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H4(S,A,z,n) is non-empty MSAlgebra over H3(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; ::_thesis: n -BitMajorityOutput (x,y) = h . n
A13: for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = H3(S,z,n) & h . (n + 1) = H1(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
for z being set st z = h . n holds
h . (n + 1) = H1(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) = H2(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
for 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) = H2(n,h1 . n) by A21;
 h = h1 from NAT_1:sch_15(A16, A17, A18, A22, A23, A24);
hence  n -BitMajorityOutput (x,y) = h . n by A19; ::_thesis: verum
end;

theorem Th7: :: FACIRC_2:7
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; ::_thesis: ( 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)] )
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
for S being non empty ManySortedSign
for 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)) ; ::_thesis: ( 0 -BitAdderCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitMajorityOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )
thus  0 -BitAdderCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1; ::_thesis: 0 -BitMajorityOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
 InnerVertices (0 -BitAdderStr (a,b)) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by A1, CIRCCOMB:42;
hence  0 -BitMajorityOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by TARSKI:def_1; ::_thesis: verum
end;

theorem Th8: :: FACIRC_2:8
for a, b being FinSequence
for 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 be FinSequence; ::_thesis: for 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) )
let c be set ; ::_thesis: ( c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] implies ( 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) ) )
assume A1: c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] ; ::_thesis: ( 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) )
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
for S being non empty ManySortedSign
for 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 A1, Def4;
 1 -BitMajorityOutput (a,b) = h . (0 + 1) by A1, A4, A5, A6, A7, Th6;
hence  ( 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) ) by A2, A3, A4, A5, A6, A7; ::_thesis: verum
end;

theorem :: FACIRC_2:9
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 ; ::_thesis: for 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) )
A1: <*a*> . 1 = a by FINSEQ_1:40;
 <*b*> . 1 = b by FINSEQ_1:40;
hence  for 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) ) by A1, Th8; ::_thesis: verum
end;

theorem Th10: :: FACIRC_2:10
for n being 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 ; ::_thesis: 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)) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
let p, q be FinSeqLen of n; ::_thesis: 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)) )
let p1, p2, q1, q2 be FinSequence; ::_thesis: ( 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)) )
deffunc H1( set , Nat) ->  Element of InnerVertices (MajorityStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = MajorityOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) ->  ManySortedSign = $1 +* (BitAdderWithOverflowStr (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2));
deffunc H3( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) ->  MSAlgebra over $1 +* (BitAdderWithOverflowStr (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $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 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A6: for n being Nat
for S being non empty ManySortedSign
for 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) = H2(S,z,n) & g1 . (n + 1) = H3(S,A,z,n) & h1 . (n + 1) = H1(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 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A12: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being 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 S1[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) );
A13: S1[ 0 ] by A3, A4, A5, A9, A10, A11;
A14: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A15: ( i <= n implies ( h1 . i = h2 . i & f1 . i = f2 . i & g1 . i = g2 . i ) ) and
A16: i + 1 <= n ; ::_thesis: ( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
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 S2[ set , set , set , set ] means verum;
A26: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f1 . 0 & A = g1 . 0 & x = h1 . 0 & S2[S,A,x, 0 ] ) by A3, A4;
A27: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . n & A = g1 . n & x = h1 . n & S2[S,A,x,n] holds
S2[H2(S,x,n),H3(S,A,x,n),H1(x,n),n + 1] ;
A28: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H3(S,A,z,n) is non-empty MSAlgebra over H2(S,z,n) ;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . n & A = g1 . n & S2[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 ; ::_thesis: ( f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) )
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 ; ::_thesis: g1 . (i + 1) = g2 . (i + 1)
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 ; ::_thesis: verum
end;
A31: for i being Nat holds S1[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; ::_thesis: n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2))
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  n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) by A31, A32; ::_thesis: verum
end;

theorem :: FACIRC_2:11
for n being 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 ; ::_thesis: 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))) )
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
let x, y be FinSeqLen of n; ::_thesis: 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))) )
let a, b be set ; ::_thesis: ( (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))) )
set p = x ^ <*a*>;
set q = y ^ <*b*>;
consider f, g, h being ManySortedSet of NAT  such that
A1: n -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>)) = f . n and
A2: n -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>)) = 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 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A6: for n being Nat
for S being non empty ManySortedSign
for 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 ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & h . (n + 1) = MajorityOutput (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (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: (x ^ <*a*>) . (n + 1) = a by A11, FINSEQ_1:42;
A14: (y ^ <*b*>) . (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 ((x ^ <*a*>),(y ^ <*b*>)) = n -BitAdderStr (x,y) by A15, Th10;
A18: n -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>)) = n -BitAdderCirc (x,y) by A15, A16, Th10;
 n -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>)) = n -BitMajorityOutput (x,y) by A15, A16, Th10;
hence  ( (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))) ) by A1, A2, A6, A7, A8, A9, A10, A13, A14, A17, A18; ::_thesis: verum
end;

theorem Th12: :: FACIRC_2:12
for n being 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 ; ::_thesis: 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))) )
let x, y be FinSequence; ::_thesis: ( (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))) )
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 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A6: for n being Nat
for S being non empty ManySortedSign
for 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) ) 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  ( (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))) ) by A1, A2, A6, A7, A8, A9; ::_thesis: verum
end;

theorem Th13: :: FACIRC_2:13
for n, m being Element of NAT st n <= m holds
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 ; ::_thesis: ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y)) )
assume A1: n <= m ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y))
let x, y be FinSequence; ::_thesis: InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y))
consider i being Nat such that
A2: m = n + i by A1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A3: m = n + i by A2;
defpred S1[ Element of NAT ] means  InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices ((n + $1) -BitAdderStr (x,y));
A4: S1[ 0 ] ;
A5: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A6: InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices ((n + j) -BitAdderStr (x,y)) ; ::_thesis: S1[j + 1]
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  S1[j + 1] by A7, A8, A9, XBOOLE_1:1; ::_thesis: verum
end;
 for j being Element of NAT holds S1[j] from NAT_1:sch_1(A4, A5);
hence  InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y)) by A3; ::_thesis: verum
end;

theorem :: FACIRC_2:14
for n being 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 ; ::_thesis: 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)))))
let x, y be FinSequence; ::_thesis: InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))
 (n + 1) -BitAdderStr (x,y) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) by Th12;
hence  InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))) by FACIRC_1:27; ::_thesis: verum
end;

definition
let k, n be Nat;
assume 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: :: FACIRC_2:def 6
 ex i being Element of NAT st
( k = i + 1 & it = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) );
uniqueness
 for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex i being Element of NAT st
( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) & ex i being Element of NAT st
( k = i + 1 & b2 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) holds
b1 = b2 ;
existence
 ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) )
proof
consider i being Nat such that
A1: k = 1 + i by X1, NAT_1:10;
reconsider n9 = n, k9 = k, i = 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: BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) 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 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) 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  ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) by A1, A2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def_6_:_
 for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b5 = (k,n) -BitAdderOutput (x,y) iff ex i being Element of NAT st
( k = i + 1 & b5 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) );

theorem :: FACIRC_2:15
for n, k being Element of NAT st k < n holds
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 ; ::_thesis: ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y))) )
assume A1: k < n ; ::_thesis: for x, y being FinSequence holds ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y)))
let x, y be FinSequence; ::_thesis: ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y)))
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  ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y))) ; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_i_being_Element_of_NAT_
for_x_being_FinSeqLen_of_i_+_1_ex_y_being_FinSeqLen_of_i_ex_a_being_set_st_x_=_y_^_<*a*>
let i be Element of NAT ; ::_thesis: for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being set st x = y ^ <*a*>
let x be FinSeqLen of i + 1; ::_thesis: ex y being FinSeqLen of i ex a being set st x = y ^ <*a*>
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 = y as FinSeqLen of i by CARD_1:def_7;
take y = y; ::_thesis: ex a being set st x = y ^ <*a*>
take a = a; ::_thesis: x = y ^ <*a*>
thus  x = y ^ <*a*> by A2; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_i_being_Element_of_NAT_
for_x_being_nonpair-yielding_FinSeqLen_of_i_+_1_ex_y_being_nonpair-yielding_FinSeqLen_of_i_ex_a_being_non_pair_set_st_x_=_y_^_<*a*>
let i be Element of NAT ; ::_thesis: for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*>
let x be nonpair-yielding FinSeqLen of i + 1; ::_thesis: ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*>
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 ; :: according to FACIRC_1:def_3 ::_thesis: ( not z in proj1 y or not y . z is pair )
assume A4: z in dom y ; ::_thesis: not y . z is pair
then  y . z = x . z by A3, FUNCT_1:47;
hence  not y . z is pair by A2, A4, FACIRC_1:def_3; ::_thesis: verum
end;
then reconsider y = 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 = a as non pair set by A6, A7, FACIRC_1:def_3;
take y = y; ::_thesis: ex a being non pair set st x = y ^ <*a*>
take a = a; ::_thesis: x = y ^ <*a*>
thus  x = y ^ <*a*> by A1; ::_thesis: verum
end;

theorem :: FACIRC_2:16
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 ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) is Relation
let x, y be FinSequence; ::_thesis: InnerVertices (n -BitAdderStr (x,y)) is Relation
defpred S1[ 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: S1[ 0 ] by FACIRC_1:38;
A2: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: InnerVertices (i -BitAdderStr (x,y)) is Relation ; ::_thesis: S1[i + 1]
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  S1[i + 1] by A3, A4, FACIRC_1:3; ::_thesis: verum
end;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2);
hence  InnerVertices (n -BitAdderStr (x,y)) is Relation ; ::_thesis: verum
end;

theorem Th17: :: FACIRC_2:17
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 ; ::_thesis: InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}
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  InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} ; ::_thesis: verum
end;

theorem Th18: :: FACIRC_2:18
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 ; ::_thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] implies InputVertices (MajorityIStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] ; ::_thesis: InputVertices (MajorityIStr (x,y,c)) = {x,y,c}
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  InputVertices (MajorityIStr (x,y,c)) = {x,y,c} ; ::_thesis: verum
end;

theorem Th19: :: FACIRC_2:19
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 ; ::_thesis: InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set Cxy = 1GateCircStr (<*x,y*>,'&');
set Cyc = 1GateCircStr (<*y,c*>,'&');
set Ccx = 1GateCircStr (<*c,x*>,'&');
set Cxyc = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
A1: 1GateCircStr (<*x,y*>,'&') tolerates ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) by CIRCCOMB:47;
A2: 1GateCircStr (<*y,c*>,'&') tolerates (1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) by CIRCCOMB:47;
A3: 1GateCircStr (<*c,x*>,'&') tolerates 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3) by CIRCCOMB:47;
A4: InnerVertices ((1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) = (InnerVertices (1GateCircStr (<*y,c*>,'&'))) \/ (InnerVertices ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) by A2, CIRCCOMB:11;
A5: InnerVertices ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) = (InnerVertices (1GateCircStr (<*c,x*>,'&'))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by A3, CIRCCOMB:11;
thus  InnerVertices (MajorityStr (x,y,c)) = InnerVertices (((1GateCircStr (<*x,y*>,'&')) +* ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&')))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:6
.= InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) by CIRCCOMB:6
.= (InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) by A1, CIRCCOMB:11
.= (InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices ((1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))))) by CIRCCOMB:6
.= ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ ((InnerVertices (1GateCircStr (<*c,x*>,'&'))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) by A4, A5, XBOOLE_1:4
.= (((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by XBOOLE_1:4
.= (({[<*x,y*>,'&']} \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:42
.= (({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:42
.= (({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:42
.= ({[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by ENUMSET1:1
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by ENUMSET1:3
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} by CIRCCOMB:42 ; ::_thesis: verum
end;

theorem Th20: :: FACIRC_2:20
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 ; ::_thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] implies InputVertices (MajorityStr (x,y,c)) = {x,y,c} )
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set S = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
A1: InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} by CIRCCOMB:42;
A2: InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by CIRCCOMB:42
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by FINSEQ_2:128 ;
set MI = MajorityIStr (x,y,c);
assume that
A3: x <> [<*y,c*>,'&'] and
A4: y <> [<*c,x*>,'&'] and
A5: c <> [<*x,y*>,'&'] ; ::_thesis: InputVertices (MajorityStr (x,y,c)) = {x,y,c}
 rng <*c,x*> = {c,x} by FINSEQ_2:127;
then A6: x in rng <*c,x*> by TARSKI:def_2;
 len <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> = 3 by FINSEQ_1:45;
then A7: Seg 3 = dom <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by FINSEQ_1:def_3;
then A8: 3 in dom <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by FINSEQ_1:1;
 <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 3 = [<*c,x*>,'&'] by FINSEQ_1:45;
then  [3,[<*c,x*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A8, FUNCT_1:1;
then  [<*c,x*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def_13;
then A9: the_rank_of [<*c,x*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,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 <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A7, FINSEQ_1:1;
 <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 1 = [<*x,y*>,'&'] by FINSEQ_1:45;
then  [1,[<*x,y*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A11, FUNCT_1:1;
then  [<*x,y*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def_13;
then A12: the_rank_of [<*x,y*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,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 <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A7, FINSEQ_1:1;
 <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 2 = [<*y,c*>,'&'] by FINSEQ_1:45;
then  [2,[<*y,c*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A14, FUNCT_1:1;
then  [<*y,c*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def_13;
then A15: the_rank_of [<*y,c*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] by CLASSES1:82;
A16: {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} = {} by XBOOLE_1:37;
A17: {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} = {x,y,c}
proof
thus  {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} c= {x,y,c} ; :: according to XBOOLE_0:def_10 ::_thesis: {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]}
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y,c} or a in {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} )
assume A18: a in {x,y,c} ; ::_thesis: a in {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]}
then  ( a = x or a = y or a = c ) by ENUMSET1:def_1;
then  a <> [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] by A6, A9, A10, A12, A13, A15, CLASSES1:82;
then  not a in {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} by TARSKI:def_1;
hence  a in {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]} by A18, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  InputVertices (MajorityStr (x,y,c)) = ((InputVertices (MajorityIStr (x,y,c))) \ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c)))) by CIRCCMB2:5, CIRCCOMB:47
.= {x,y,c} \/ ({[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \ (InnerVertices (MajorityIStr (x,y,c)))) by A1, A2, A3, A4, A5, A17, Th18
.= {x,y,c} \/ {} by A16, Th17
.= {x,y,c} ; ::_thesis: verum
end;

theorem Th21: :: FACIRC_2:21
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 ; ::_thesis: ( S1 tolerates S2 & InputVertices S1 = InputVertices S2 implies InputVertices (S1 +* S2) = InputVertices S1 )
assume that
A1: S1 tolerates S2 and
A2: InputVertices S1 = InputVertices S2 ; ::_thesis: InputVertices (S1 +* S2) = InputVertices S1
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 ; ::_thesis: verum
end;

theorem Th22: :: FACIRC_2:22
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 ; ::_thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] implies InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] and
A4: c <> [<*x,y*>,'xor'] ; ::_thesis: InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}
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  InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} by A5, Th21, CIRCCOMB:47; ::_thesis: verum
end;

theorem Th23: :: FACIRC_2:23
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 ; ::_thesis: InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))}
 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  InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))} ; ::_thesis: verum
end;

registration
cluster empty  ->  non pair for set ;
coherence
 for b1 being set st b1 is empty holds
not b1 is pair ;
end;

registration
cluster empty Relation-like Function-like  ->  nonpair-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is nonpair-yielding
proof
let F be Function; ::_thesis: ( F is empty implies F is nonpair-yielding )
assume A1: F is empty ; ::_thesis: F is nonpair-yielding
let x be set ; :: according to FACIRC_1:def_3 ::_thesis: ( not x in proj1 F or not F . x is pair )
assume  x in dom F ; ::_thesis: not F . x is pair
thus  not F . x is pair by A1; ::_thesis: verum
end;
let f be nonpair-yielding Function;
let x be set ;
clusterf . x ->  non pair ;
coherence
 not f . x is pair
proof
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: not f . x is pair
hence  not f . x is pair by FACIRC_1:def_3; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: not f . x is pair
hence  not f . x is pair by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;

registration
let n be Element of NAT ;
let x, y be FinSequence;
clustern -BitMajorityOutput (x,y) ->  pair ;
coherence
 n -BitMajorityOutput (x,y) is pair
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
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) by Def5;
defpred S1[ Element of NAT ] means n -BitMajorityOutput (x,y) is pair ;
A2: S1[ 0 ] by A1;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
(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  ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A3);
hence  n -BitMajorityOutput (x,y) is pair ; ::_thesis: verum
end;
end;

theorem Th24: :: FACIRC_2:24
for x, y being FinSequence
for 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; ::_thesis: for 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 ) )
defpred S1[ 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: S1[ 0 ] by A1, MCART_1:7;
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
set c = n -BitMajorityOutput (x,y);
A4: (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] ;
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)),(n -BitMajorityOutput (x,y))*>,'&'],[<*(n -BitMajorityOutput (x,y)),(x . (n + 1))*>,'&']*> by A4, MCART_1:7;
hence  S1[n + 1] by A4, A5, FINSEQ_1:45, MCART_1:7; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A3); ::_thesis: verum
end;

theorem Th25: :: FACIRC_2:25
for n being Element of NAT
for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
let x, y be FinSequence; ::_thesis: for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
let p be set ; ::_thesis: ( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
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  ( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] ) by A3, A4, FINSEQ_2:110; ::_thesis: verum
end;

theorem Th26: :: FACIRC_2:26
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; ::_thesis: 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 )
deffunc H1( Nat) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitAdderStr (f,g);
deffunc H2( set , Nat) ->  ManySortedSign = BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H3( Nat) ->  Element of InnerVertices ($1 -BitAdderStr (f,g)) = $1 -BitMajorityOutput (f,g);
consider h being ManySortedSet of NAT  such that
A1: for n being Element of NAT holds h . n = H3(n) from PBOOLE:sch_5();
deffunc H4( Nat) ->  set = h . $1;
deffunc H5( set , Nat) ->  Element of InnerVertices (MajorityStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = MajorityOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set k = (0 -tuples_on BOOLEAN) --> FALSE;
A2: 0 -BitAdderStr (f,g) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th7;
then A3: InnerVertices H1( 0 ) is Relation by FACIRC_1:38;
A4: InputVertices H1( 0 ) is without_pairs by A2, FACIRC_1:39;
 H4( 0 ) = 0 -BitMajorityOutput (f,g) by A1;
then A5: h . 0 in InnerVertices H1( 0 ) ;
A6: for n being Nat
for x being set holds InnerVertices H2(x,n) is Relation by FACIRC_1:88;
A7: now__::_thesis:_for_n_being_Nat
for_x_being_set_st_x_=_H4(n)_holds_
InputVertices_H2(x,n)_=_{(f_._(n_+_1)),(g_._(n_+_1)),x}
let n be Nat; ::_thesis: for x being set st x = H4(n) holds
InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}
let x be set ; ::_thesis: ( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} )
assume A8: x = H4(n) ; ::_thesis: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}
A9: n in NAT by ORDINAL1:def_12;
then A10: H4(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 H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A11, Th22; ::_thesis: verum
end;
A12: for n being Nat
for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
proof
let n be Nat; ::_thesis: for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
let x be set ; ::_thesis: ( x = h . n implies (InputVertices H2(x,n)) \ {x} is without_pairs )
assume  x = H4(n) ; ::_thesis: (InputVertices H2(x,n)) \ {x} is without_pairs
then A13: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7;
thus  (InputVertices H2(x,n)) \ {x} is without_pairs ::_thesis: verum
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H2(x,n)) \ {x}
assume A14: a in (InputVertices H2(x,n)) \ {x} ; ::_thesis: contradiction
then  a in InputVertices H2(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; ::_thesis: verum
end;
end;
A16: now__::_thesis:_for_n_being_Nat
for_S_being_non_empty_ManySortedSign_
for_x_being_set_st_S_=_H1(n)_&_x_=_h_._n_holds_
(_H1(n_+_1)_=_S_+*_H2(x,n)_&_h_._(n_+_1)_=_H5(x,n)_&_x_in_InputVertices_H2(x,n)_&_H5(x,n)_in_InnerVertices_H2(x,n)_)
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for x being set st S = H1(n) & x = h . n holds
( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for x being set st S = H1(n) & x = h . n holds
( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
let x be set ; ::_thesis: ( S = H1(n) & x = h . n implies ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) )
A17: n in NAT by ORDINAL1:def_12;
assume that
A18: S = H1(n) and
A19: x = h . n ; ::_thesis: ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
A20: x = n -BitMajorityOutput (f,g) by A1, A17, A19;
A21: H4(n + 1) = (n + 1) -BitMajorityOutput (f,g) by A1;
thus  H1(n + 1) = S +* H2(x,n) by A17, A18, A20, Th12; ::_thesis: ( h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
thus  h . (n + 1) = H5(x,n) by A17, A20, A21, Th12; ::_thesis: ( x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) )
 InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A19;
hence  x in InputVertices H2(x,n) by ENUMSET1:def_1; ::_thesis: H5(x,n) in InnerVertices H2(x,n)
A22: InnerVertices H2(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;
 H5(x,n) in {H5(x,n)} by TARSKI:def_1;
hence  H5(x,n) in InnerVertices H2(x,n) by A22, XBOOLE_0:def_3; ::_thesis: verum
end;
A23: for n being Nat holds
( InputVertices H1(n + 1) = (InputVertices H1(n)) \/ ((InputVertices H2(h . n,n)) \ {(h . n)}) & InnerVertices H1(n) is Relation & InputVertices H1(n) is without_pairs ) from CIRCCMB2:sch_11(A3, A4, A5, A6, A12, A16);
let n be Element of NAT ; ::_thesis: ( 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 )
 h . n = n -BitMajorityOutput (f,g) by A1;
hence  ( 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 ) by A23; ::_thesis: verum
end;

theorem :: FACIRC_2:27
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 S1[ Element of NAT ] means  for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitAdderStr (x,y)) = (rng x) \/ (rng y);
A1: S1[ 0 ]
proof
let x, y be nonpair-yielding FinSeqLen of 0 ; ::_thesis: InputVertices (0 -BitAdderStr (x,y)) = (rng x) \/ (rng y)
set f = (0 -tuples_on BOOLEAN) --> FALSE;
 0 -BitAdderStr (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th7;
hence  InputVertices (0 -BitAdderStr (x,y)) = (rng x) \/ (rng y) by CIRCCOMB:42; ::_thesis: verum
end;
A2: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; ::_thesis: S1[i + 1]
let x, y be nonpair-yielding FinSeqLen of i + 1; ::_thesis: InputVertices ((i + 1) -BitAdderStr (x,y)) = (rng x) \/ (rng y)
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 ((i + 1) -BitAdderStr (x,y)) = (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 ;
::_thesis: verum
end;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2); ::_thesis: verum
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 ; ::_thesis: 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 )
let s be State of (MajorityCirc (x,y,c)); ::_thesis: 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 )
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 ) )
assume that
A1: a1 = s . x and
A2: a2 = s . y and
A3: a3 = s . c ; ::_thesis: ( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )
set S = MajorityStr (x,y,c);
A4: InnerVertices (MajorityStr (x,y,c)) = the carrier' of (MajorityStr (x,y,c)) by FACIRC_1:37;
A5: dom s = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
A6: x in the carrier of (MajorityStr (x,y,c)) by FACIRC_1:72;
A7: y in the carrier of (MajorityStr (x,y,c)) by FACIRC_1:72;
A8: c in the carrier of (MajorityStr (x,y,c)) 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 ;
::_thesis: ( (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )
 [<*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 ;
::_thesis: (Following s) . [<*c,x*>,'&'] = a3 '&' a1
 [<*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 ;
::_thesis: verum
end;

theorem Th28: :: FACIRC_2:28
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 ; ::_thesis: 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
let s be State of (MajorityCirc (x,y,c)); ::_thesis: 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
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . [<*x,y*>,'&'] & a2 = s . [<*y,c*>,'&'] & a3 = s . [<*c,x*>,'&'] implies (Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3 )
assume that
A1: a1 = s . [<*x,y*>,'&'] and
A2: a2 = s . [<*y,c*>,'&'] and
A3: a3 = s . [<*c,x*>,'&'] ; ::_thesis: (Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set S = MajorityStr (x,y,c);
A4: InnerVertices (MajorityStr (x,y,c)) = the carrier' of (MajorityStr (x,y,c)) by FACIRC_1:37;
A5: dom s = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
reconsider xy = [<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'] as Element of InnerVertices (MajorityStr (x,y,c)) 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 ; ::_thesis: verum
end;

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

theorem Th29: :: FACIRC_2:29
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] implies for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable )
set S = MajorityStr (x,y,c);
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] ; ::_thesis: for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
let s be State of (MajorityCirc (x,y,c)); ::_thesis: Following (s,2) is stable
A4: dom (Following (Following (s,2))) = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
A5: dom (Following (s,2)) = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
reconsider xx = x, yy = y, cc = c as Vertex of (MajorityStr (x,y,c)) by FACIRC_1:72;
set a1 = s . xx;
set a2 = s . yy;
set a3 = s . cc;
set ffs = Following (s,2);
set fffs = Following (Following (s,2));
A6: s . xx = s . x ;
A7: s . yy = s . y ;
A8: s . cc = s . c ;
A9: (Following (s,2)) . (MajorityOutput (x,y,c)) = (((s . xx) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' ((s . cc) '&' (s . xx)) by A1, A2, A3, Lm4;
A10: (Following (s,2)) . [<*x,y*>,'&'] = (s . xx) '&' (s . yy) by A1, A2, A3, A8, Lm4;
A11: (Following (s,2)) . [<*y,c*>,'&'] = (s . yy) '&' (s . cc) by A1, A2, A3, A6, Lm4;
A12: (Following (s,2)) . [<*c,x*>,'&'] = (s . cc) '&' (s . xx) by A1, A2, A3, A7, Lm4;
A13: Following (s,2) = Following (Following s) by FACIRC_1:15;
A14: InputVertices (MajorityStr (x,y,c)) = {x,y,c} by A1, A2, A3, Th20;
then A15: x in InputVertices (MajorityStr (x,y,c)) by ENUMSET1:def_1;
A16: y in InputVertices (MajorityStr (x,y,c)) by A14, ENUMSET1:def_1;
A17: c in InputVertices (MajorityStr (x,y,c)) by A14, ENUMSET1:def_1;
A18: (Following s) . x = s . xx by A15, CIRCUIT2:def_5;
A19: (Following s) . y = s . yy by A16, CIRCUIT2:def_5;
A20: (Following s) . c = s . cc by A17, CIRCUIT2:def_5;
A21: (Following (s,2)) . x = s . xx by A13, A15, A18, CIRCUIT2:def_5;
A22: (Following (s,2)) . y = s . yy by A13, A16, A19, CIRCUIT2:def_5;
A23: (Following (s,2)) . c = s . cc by A13, A17, A20, CIRCUIT2:def_5;
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(MajorityStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( a in the carrier of (MajorityStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume A24: a in the carrier of (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then reconsider v = a as Vertex of (MajorityStr (x,y,c)) ;
A25: v in (InputVertices (MajorityStr (x,y,c))) \/ (InnerVertices (MajorityStr (x,y,c))) by A24, XBOOLE_1:45;
thus  (Following (s,2)) . a = (Following (Following (s,2))) . a ::_thesis: verum
proof
percases ( v in InputVertices (MajorityStr (x,y,c)) or v in InnerVertices (MajorityStr (x,y,c)) ) by A25, XBOOLE_0:def_3;
suppose v in InputVertices (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
hence  (Following (s,2)) . a = (Following (Following (s,2))) . a by CIRCUIT2:def_5; ::_thesis: verum
end;
suppose v in InnerVertices (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
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  (Following (s,2)) . a = (Following (Following (s,2))) . a by A9, A10, A11, A12, A21, A22, A23, Lm3, Th28; ::_thesis: verum
end;
end;
end;
end;
hence  Following (s,2) = Following (Following (s,2)) by A4, A5, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

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

theorem Th31: :: FACIRC_2:31
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable
proof
let x, y, c be set ; ::_thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] implies for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable )
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] and
A4: c <> [<*x,y*>,'xor'] ; ::_thesis: for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable
set S = BitAdderWithOverflowStr (x,y,c);
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
set A = BitAdderWithOverflowCirc (x,y,c);
set A1 = BitAdderCirc (x,y,c);
set A2 = MajorityCirc (x,y,c);
let s be State of (BitAdderWithOverflowCirc (x,y,c)); ::_thesis: Following (s,2) is stable
reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitAdderCirc (x,y,c)) by FACIRC_1:26;
reconsider s2 = s | the carrier of (MajorityStr (x,y,c)) as State of (MajorityCirc (x,y,c)) by FACIRC_1:26;
reconsider t = s as State of ((BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c))) ;
 InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} by A4, FACIRC_1:57;
then A5: InputVertices (2GatesCircStr (x,y,c,'xor')) = InputVertices (MajorityStr (x,y,c)) by A1, A2, A3, Th20;
A6: InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by XBOOLE_1:79;
A7: InnerVertices (MajorityStr (x,y,c)) misses InputVertices (MajorityStr (x,y,c)) by XBOOLE_1:79;
then A8: Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) by A5, FACIRC_1:30;
A9: Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) by A5, A7, FACIRC_1:30;
A10: Following (s2,2) = (Following (t,2)) | the carrier of (MajorityStr (x,y,c)) by A5, A6, FACIRC_1:31;
A11: Following (s2,3) = (Following (t,3)) | the carrier of (MajorityStr (x,y,c)) 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 (BitAdderWithOverflowStr (x,y,c)) by CIRCUIT1:3;
A16: dom (Following (s,3)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) by CIRCUIT1:3;
A17: dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;
A18: dom (Following (s2,2)) = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
A19: the carrier of (BitAdderWithOverflowStr (x,y,c)) = the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (MajorityStr (x,y,c)) by CIRCCOMB:def_2;
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BitAdderWithOverflowStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( a in the carrier of (BitAdderWithOverflowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume  a in the carrier of (BitAdderWithOverflowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then  ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (MajorityStr (x,y,c)) ) 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; ::_thesis: verum
end;
hence  Following (s,2) = Following (Following (s,2)) by A14, A15, A16, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
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 ; ::_thesis: ex N being Function of NAT,NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n )
defpred S1[ set ] means $1 = 0 ;
deffunc H1( set ) ->  Element of NAT = 1;
deffunc H2( set ) ->  Element of NAT = 2;
consider N0 being Function such that
 dom N0 = NAT and
A1: for i being set st i in NAT holds
( ( S1[i] implies N0 . i = H1(i) ) & ( not S1[i] implies N0 . i = H2(i) ) ) from PARTFUN1:sch_1();
defpred S2[ set ] means $1 <> 2;
deffunc H3( set ) ->  set = N0 . $1;
deffunc H4( set ) ->  Element of NAT = n;
consider N being Function such that
A2: dom N = NAT and
A3: for i being set st i in NAT holds
( ( S2[i] implies N . i = H3(i) ) & ( not S2[i] implies N . i = H4(i) ) ) from PARTFUN1:sch_1();
 rng N c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng N or x in NAT )
assume  x in rng N ; ::_thesis: x in NAT
then consider i being set  such that
A4: i in dom N and
A5: x = N . i by FUNCT_1:def_3;
reconsider i = 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  x in NAT ; ::_thesis: verum
end;
then reconsider N = N as Function of NAT,NAT by A2, FUNCT_2:2;
take  N ; ::_thesis: ( N . 0 = 1 & N . 1 = 2 & N . 2 = n )
A6: N . 0 = N0 . 0 by A3;
 N0 . 1 = N . 1 by A3;
hence  ( N . 0 = 1 & N . 1 = 2 ) by A1, A6; ::_thesis: N . 2 = n
thus  N . 2 = n by A3; ::_thesis: verum
end;

theorem :: FACIRC_2:32
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 ; ::_thesis: 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
let f, g be nonpair-yielding FinSeqLen of n; ::_thesis: for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable
deffunc H1( set , Nat) ->  ManySortedSign = BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H2( set , Nat) ->  MSAlgebra over BitAdderWithOverflowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitAdderWithOverflowCirc ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H3( set , Nat) ->  Element of InnerVertices (MajorityStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = 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 H4( Element of NAT ) ->  Element of NAT = N . $1;
A4: for x being set
for n being Nat holds H2(x,n) is strict gate`2=den Boolean Circuit of H1(x,n) ;
A5: now__::_thesis:_for_s_being_State_of_(1GateCircuit_(<*>,((0_-tuples_on_BOOLEAN)_-->_FALSE)))_holds_Following_(s,H4(_0_))_is_stable
let s be State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))); ::_thesis: Following (s,H4( 0 )) is stable
 Following (s,1) = Following s by FACIRC_1:14;
hence  Following (s,H4( 0 )) is stable by A1, CIRCCMB2:2; ::_thesis: verum
end;
deffunc H5( Element of NAT ) ->  Element of InnerVertices ($1 -BitAdderStr (f,g)) = $1 -BitMajorityOutput (f,g);
consider h being ManySortedSet of NAT  such that
A6: for n being Element of NAT holds h . n = H5(n) from PBOOLE:sch_5();
A7: for n being Nat
for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
proof
let n be Nat; ::_thesis: for x being set
for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
let x be set ; ::_thesis: for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds
for s being State of A holds Following (s,H4(1)) is stable
let A be non-empty Circuit of H1(x,n); ::_thesis: ( x = h . n & A = H2(x,n) implies for s being State of A holds Following (s,H4(1)) is stable )
A8: n in NAT by ORDINAL1:def_12;
assume  x = h . n ; ::_thesis: ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable )
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  ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) by A2, A10, Th31; ::_thesis: verum
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
for S being non empty ManySortedSign
for 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__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
h1_._i_=_h_._i
let i be set ; ::_thesis: ( i in NAT implies h1 . i = h . i )
assume  i in NAT ; ::_thesis: h1 . i = h . i
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 ; ::_thesis: verum
end;
then A17: h1 = h by PBOOLE:3;
A18: ex u, v being ManySortedSet of NAT st
( n -BitAdderStr (f,g) = u . H4(2) & n -BitAdderCirc (f,g) = v . H4(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( u . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
proof
take  f1 ; ::_thesis: ex v being ManySortedSet of NAT st
( n -BitAdderStr (f,g) = f1 . H4(2) & n -BitAdderCirc (f,g) = v . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
take  g1 ; ::_thesis: ( n -BitAdderStr (f,g) = f1 . H4(2) & n -BitAdderCirc (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) )
thus  ( n -BitAdderStr (f,g) = f1 . H4(2) & n -BitAdderCirc (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitMajorityOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds
( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) by A3, A6, A11, A12, A13, A14, A16, A17; ::_thesis: verum
end;
A19: ( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is Relation & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is without_pairs ) by FACIRC_1:38, FACIRC_1:39;
A20: [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = 0 -BitMajorityOutput (f,g) by Th7;
 InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42;
then A21: ( h . 0 = 0 -BitMajorityOutput (f,g) & 0 -BitMajorityOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) ) by A6, A20, TARSKI:def_1;
A22: for n being Nat
for x being set holds InnerVertices H1(x,n) is Relation by FACIRC_1:88;
A23: for n being Nat
for x being set st x = h . n holds
(InputVertices H1(x,n)) \ {x} is without_pairs
proof
let n be Nat; ::_thesis: for x being set st x = h . n holds
(InputVertices H1(x,n)) \ {x} is without_pairs
let x be set ; ::_thesis: ( x = h . n implies (InputVertices H1(x,n)) \ {x} is without_pairs )
assume A24: x = h . n ; ::_thesis: (InputVertices H1(x,n)) \ {x} is without_pairs
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 H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A27, Th22;
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H1(x,n)) \ {x}
assume A29: a in (InputVertices H1(x,n)) \ {x} ; ::_thesis: contradiction
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  contradiction by A31, TARSKI:def_1; ::_thesis: verum
end;
A32: for n being Nat
for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
proof
let n be Nat; ::_thesis: for x being set st x = h . n holds
( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
let x be set ; ::_thesis: ( x = h . n implies ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) )
assume A33: x = h . n ; ::_thesis: ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,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) = H3(x,n) by A34, A35, Th12; ::_thesis: ( x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) )
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 H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A36, Th22;
hence  x in InputVertices H1(x,n) by ENUMSET1:def_1; ::_thesis: H3(x,n) in InnerVertices H1(x,n)
set xx = f . (n + 1);
set xy = g . (n + 1);
A37: H3(x,n) in {H3(x,n)} by TARSKI:def_1;
 InnerVertices H1(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;
hence  H3(x,n) in InnerVertices H1(x,n) by A37, XBOOLE_0:def_3; ::_thesis: verum
end;
 for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(H4( 0 ) + (H4(2) * H4(1)))) is stable from CIRCCMB2:sch_22(A4, A5, A7, A18, A19, A21, A22, A23, A32);
hence  for s being State of (n -BitAdderCirc (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; ::_thesis: verum
end;

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

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

theorem :: FACIRC_2:35
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;