let f, g be nonpair-yielding FinSequence; for n being 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();
A2:
for n being Nat holds h . n = H3(n)
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;
A3:
0 -BitAdderStr (f,g) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
by Th7;
then A4:
InnerVertices H1( 0 ) is Relation
by FACIRC_1:38;
A5:
InputVertices H1( 0 ) is without_pairs
by A3, FACIRC_1:39;
H4( 0 ) = 0 -BitMajorityOutput (f,g)
by A2;
then A6:
h . 0 in InnerVertices H1( 0 )
;
A7:
for n being Nat
for x being set holds InnerVertices H2(x,n) is Relation
by FACIRC_1:88;
A8:
now 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;
for x being set st x = H4(n) holds
InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}let x be
set ;
( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} )assume A9:
x = H4(
n)
;
InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}A10:
H4(
n)
= n -BitMajorityOutput (
f,
g)
by A2;
then A11:
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&']
by A9, Th25;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor']
by A9, A10, Th25;
hence
InputVertices H2(
x,
n)
= {(f . (n + 1)),(g . (n + 1)),x}
by A11, Th22;
verum end;
A12:
for n being Nat
for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
A16:
now 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;
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 ;
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 ;
( 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) ) )assume that A17:
S = H1(
n)
and A18:
x = h . n
;
( 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) )A19:
x = n -BitMajorityOutput (
f,
g)
by A2, A18;
A20:
H4(
n + 1)
= (n + 1) -BitMajorityOutput (
f,
g)
by A2;
thus
H1(
n + 1)
= S +* H2(
x,
n)
by A17, A19, Th12;
( 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 A19, A20, Th12;
( 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 A8, A18;
hence
x in InputVertices H2(
x,
n)
by ENUMSET1:def 1;
H5(x,n) in InnerVertices H2(x,n)A21:
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 A21, XBOOLE_0:def 3;
verum end;
A22:
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(A4, A5, A6, A7, A12, A16);
let n be Nat; ( 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 A2;
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 A22; verum