let n be Nat; :: thesis:
let f, g be nonpair-yielding FinSeqLen of n; :: thesis:
deffunc H₁( set , Nat) -> ManySortedSign = BitGFA1Str ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₂( set , Nat) -> MSAlgebra over BitGFA1Str ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitGFA1Circ ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₃( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = GFA1CarryOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
set N = (1,2) followed_by (In (n,NAT));
A1: ((1,2) followed_by (In (n,NAT))) . 0 = 1 by FUNCT_7:122;
A2: ((1,2) followed_by (In (n,NAT))) . 1 = 2 by FUNCT_7:123;
A3: ((1,2) followed_by (In (n,NAT))) . 2 = n by FUNCT_7:124;
deffunc H₄( Nat) -> Element of NAT = ((1,2) followed_by (In (n,NAT))) . $1;
A4: for x being set
for n being Nat holds H₂(x,n) is strict gate`2=den Boolean Circuit of H₁(x,n) ;

end;

deffunc H₅( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (f,g)) = $1 -BitGFA1CarryOutput (f,g);
consider h being ManySortedSet of NAT such that
A6: for n being Element of NAT holds h . n = H₅(n) from PBOOLE:sch 5();
A7: 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

set f1 = and2c ;
set f0 = xor2c ;
let n be Nat; :: thesis:
let x be set ; :: thesis:
let A be non-empty Circuit of H₁(x,n); :: thesis:
assume A8: x = h . n ; :: thesis:
n in NAT by ORDINAL1:def 12;
then A9: x = H₅(n) by A6, A8;
then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by Lm4;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A9, Lm4;
hence ( not A = H₂(x,n) or for s being State of A holds Following (s,H₄(1)) is stable ) by A2, A10, GFACIRC1:72; :: thesis:

end;

set Sn = n -BitGFA1Str (f,g);
set An = n -BitGFA1Circ (f,g);
set o0 = 0 -BitGFA1CarryOutput (f,g);
consider f1, g1, h1 being ManySortedSet of NAT such that
A11: n -BitGFA1Str (f,g) = f1 . n and
A12: n -BitGFA1Circ (f,g) = g1 . n and
A13: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A14: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A15: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] 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 +* H₁(z,n) & g1 . (n + 1) = A +* H₂(z,n) & h1 . (n + 1) = H₃(z,n) ) by Def6;

let i be object ; :: thesis:
assume A17: i in NAT ; :: thesis:
then reconsider j = i as Nat ;
thus h1 . i = H₅(j) by A13, A14, A15, A16, Th15
.= h . i by A6, A17 ; :: thesis:

end;

then A18: h1 = h by PBOOLE:3;
A19: ex u, v being ManySortedSet of NAT st
( n -BitGFA1Str (f,g) = u . H₄(2) & n -BitGFA1Circ (f,g) = v . H₄(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (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 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) ) ) )

take f1 ; :: thesis:
take g1 ; :: thesis:
thus ( n -BitGFA1Str (f,g) = f1 . H₄(2) & n -BitGFA1Circ (f,g) = g1 . H₄(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (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 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 A3, A6, A11, A12, A13, A14, A16, A18; :: thesis:

end;

end;

A32: 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) )

set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f0 = xor2c ;
let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A33: x = h . n ; :: thesis:
n in NAT by ORDINAL1:def 12;
then A34: x = H₅(n) by A6, A33;
h . (n + 1) = H₅(n + 1) by A6;
hence h . (n + 1) = H₃(x,n) by A34, Th21; :: thesis:
A35: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by A34, Lm4;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A34, Lm4;
then InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A35, GFACIRC1:65;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis:
A36: InnerVertices H₁(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2c]} \/ {(GFA1AdderOutput ((f . (n + 1)),(g . (n + 1)),x))}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2c],[<*(g . (n + 1)),x*>,and2a],[<*x,(f . (n + 1))*>,and2]}) \/ {(GFA1CarryOutput ((f . (n + 1)),(g . (n + 1)),x))} by GFACIRC1:63;
H₃(x,n) in {H₃(x,n)} by TARSKI:def 1;
hence H₃(x,n) in InnerVertices H₁(x,n) by A36, XBOOLE_0:def 3; :: thesis:

end;

for s being State of (n -BitGFA1Circ (f,g)) holds Following (s,(H₄( 0 ) + (H₄(2) * H₄(1)))) is stable from CIRCCMB2:sch 22(A4, A5, A7, A19, A20, A22, A23, A24, A32);
hence for s being State of (n -BitGFA1Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; :: thesis: