let n be Element of NAT ; :: thesis: for x, y being nonpair-yielding FinSeqLen of
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 ; :: thesis: for s being State of (n -BitAdderCirc f,g) holds Following s,(1 + (2 * n)) is stable
deffunc H₁( set , Nat) -> ManySortedSign = BitAdderWithOverflowStr (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₂( set , Nat) -> MSAlgebra of BitAdderWithOverflowStr (f . ($2 + 1)),(g . ($2 + 1)),$1 = BitAdderWithOverflowCirc (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₃( 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 & N . 1 = 2 & N . 2 = n ) by Lm5;
deffunc H₄( Element of NAT ) -> Element of NAT = N . $1;
A2: for x being set
for n being Nat holds H₂(x,n) is strict gate`2=den Boolean Circuit of H₁(x,n) ;

A3: now

let s be State of (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )); :: thesis: Following s,H₄( 0 ) is stable
Following s,1 = Following s by FACIRC_1:14;
hence Following s,H₄( 0 ) is stable by A1, CIRCCMB2:2; :: thesis: verum

end;

deffunc H₅( Element of NAT ) -> Element of InnerVertices ($1 -BitAdderStr f,g) = $1 -BitMajorityOutput f,g;
consider h being ManySortedSet of such that
A4: for n being Element of NAT holds h . n = H₅(n) from PBOOLE:sch 5();
A5: for n being Nat
for x being set
for A being non-empty Circuit of H₁(x,n) st x = h . n & A = H₂(x,n) holds
for s being State of A holds Following s,H₄(1) is stable

proof

let n be Nat; :: thesis: for x being set
for A being non-empty Circuit of H₁(x,n) st x = h . n & A = H₂(x,n) holds
for s being State of A holds Following s,H₄(1) is stable
let x be set ; :: thesis: for A being non-empty Circuit of H₁(x,n) st x = h . n & A = H₂(x,n) holds
for s being State of A holds Following s,H₄(1) is stable
let A be non-empty Circuit of H₁(x,n); :: thesis: ( x = h . n & A = H₂(x,n) implies for s being State of A holds Following s,H₄(1) is stable )
X: n in NAT by ORDINAL1:def 13;
assume x = h . n ; :: thesis: ( not A = H₂(x,n) or for s being State of A holds Following s,H₄(1) is stable )
then x = n -BitMajorityOutput f,g by A4, X;
then ( f . (n + 1) <> [<*(g . (n + 1)),x*>,'&' ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor' ] ) by Th26, X;
hence ( not A = H₂(x,n) or for s being State of A holds Following s,H₄(1) is stable ) by A1, Th32; :: 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 such that
A6: ( n -BitAdderStr f,g = f1 . n & n -BitAdderCirc f,g = g1 . n ) and
A7: ( f1 . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g1 . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h1 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds
( f1 . (n + 1) = S +* (BitAdderWithOverflowStr (f . (n + 1)),(g . (n + 1)),z) & g1 . (n + 1) = A +* (BitAdderWithOverflowCirc (f . (n + 1)),(g . (n + 1)),z) & h1 . (n + 1) = MajorityOutput (f . (n + 1)),(g . (n + 1)),z ) ) ) by Def4;

now

let i be set ; :: 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 A7, Th7
.= h . i by A4 ; :: thesis: verum

end;

then A8: h1 = h by PBOOLE:3;
A9: ex u, v being ManySortedSet of st
( n -BitAdderStr f,g = u . H₄(2) & n -BitAdderCirc f,g = v . H₄(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 of S
for x being set
for A2 being non-empty MSAlgebra of H₁(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H₂(x,n) holds
( u . (n + 1) = S +* H₁(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) )

proof

take f1 ; :: thesis: ex v being ManySortedSet of st
( n -BitAdderStr f,g = f1 . H₄(2) & n -BitAdderCirc f,g = v . H₄(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 of S
for x being set
for A2 being non-empty MSAlgebra of H₁(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H₂(x,n) holds
( f1 . (n + 1) = S +* H₁(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) )
take g1 ; :: thesis: ( n -BitAdderStr f,g = f1 . H₄(2) & n -BitAdderCirc f,g = g1 . H₄(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 of S
for x being set
for A2 being non-empty MSAlgebra of H₁(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H₂(x,n) holds
( f1 . (n + 1) = S +* H₁(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) )
thus ( n -BitAdderStr f,g = f1 . H₄(2) & n -BitAdderCirc f,g = g1 . H₄(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 of S
for x being set
for A2 being non-empty MSAlgebra of H₁(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H₂(x,n) holds
( f1 . (n + 1) = S +* H₁(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) ) by A1, A4, A6, A7, A8; :: thesis: verum

end;

A10: ( InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) is Relation & not InputVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) is with_pair ) by FACIRC_1:38, FACIRC_1:39;
( [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] = 0 -BitMajorityOutput f,g & InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) = {[<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )]} ) by Th8, CIRCCOMB:49;
then A11: ( h . 0 = 0 -BitMajorityOutput f,g & 0 -BitMajorityOutput f,g in InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) ) by A4, TARSKI:def 1;
A12: for n being Nat
for x being set holds InnerVertices H₁(x,n) is Relation by FACIRC_1:88;
A13: for n being Nat
for x being set st x = h . n holds
not (InputVertices H₁(x,n)) \ {x} is with_pair

proof

let n be Nat; :: thesis: for x being set st x = h . n holds
not (InputVertices H₁(x,n)) \ {x} is with_pair
let x be set ; :: thesis: ( x = h . n implies not (InputVertices H₁(x,n)) \ {x} is with_pair )
assume A14: x = h . n ; :: thesis: not (InputVertices H₁(x,n)) \ {x} is with_pair
X: n in NAT by ORDINAL1:def 13;
then x = n -BitMajorityOutput f,g by A4, A14;
then ( f . (n + 1) <> [<*(g . (n + 1)),x*>,'&' ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor' ] ) by Th26, X;
then A15: InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by Th23;
let a be pair set ; :: according to FACIRC_1:def 2 :: thesis: not a in (InputVertices H₁(x,n)) \ {x}
assume a in (InputVertices H₁(x,n)) \ {x} ; :: thesis: contradiction
then ( a in {(f . (n + 1)),(g . (n + 1)),x} & not a in {x} ) by A15, XBOOLE_0:def 5;
then ( ( a = f . (n + 1) or a = g . (n + 1) or a = x ) & a <> x ) by ENUMSET1:def 1, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

A16: for n being Nat
for x being set st x = h . n holds
( h . (n + 1) = H₃(x,n) & x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )

proof

let n be Nat; :: thesis: for x being set st x = h . n holds
( h . (n + 1) = H₃(x,n) & x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )
let x be set ; :: thesis: ( x = h . n implies ( h . (n + 1) = H₃(x,n) & x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) ) )
assume A17: x = h . n ; :: thesis: ( h . (n + 1) = H₃(x,n) & x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )
X: n in NAT by ORDINAL1:def 13;
A18: ( x = n -BitMajorityOutput f,g & h . (n + 1) = (n + 1) -BitMajorityOutput f,g ) by A4, A17, X;
hence h . (n + 1) = H₃(x,n) by Th13, X; :: thesis: ( x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )
( f . (n + 1) <> [<*(g . (n + 1)),x*>,'&' ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor' ] ) by A18, Th26, X;
then InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by Th23;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis: H₃(x,n) in InnerVertices H₁(x,n)
set xx = f . (n + 1);
set xy = g . (n + 1);
A19: H₃(x,n) in {H₃(x,n)} by TARSKI:def 1;
InnerVertices H₁(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 Th24;
hence H₃(x,n) in InnerVertices H₁(x,n) by A19, XBOOLE_0:def 3; :: thesis: verum

end;

for s being State of (n -BitAdderCirc f,g) holds Following s,(H₄( 0 ) + (H₄(2) * H₄(1))) is stable from CIRCCMB2:sch 22(A2, A3, A5, A9, A10, A11, A12, A13, A16);
hence for s being State of (n -BitAdderCirc f,g) holds Following s,(1 + (2 * n)) is stable by A1; :: thesis: verum