let n be Nat; :: thesis:
let f, g be nonpair-yielding FinSeqLen of n; :: thesis:
deffunc H₁( set , Nat) -> ManySortedSign = BitGFA0Str (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₂( set , Nat) -> MSAlgebra of BitGFA0Str (f . ($2 + 1)),(g . ($2 + 1)),$1 = BitGFA0Circ (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₃( set , Nat) -> Element of InnerVertices (GFA0CarryStr (f . ($2 + 1)),(g . ($2 + 1)),$1) = GFA0CarryOutput (f . ($2 + 1)),(g . ($2 + 1)),$1;
set S0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE );
set A0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE );
set h0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )];
n in NAT by ORDINAL1:def 13;
then consider N being Function of NAT ,NAT such that
A1: N . 0 = 1 and
A2: N . 1 = 2 and
A3: N . 2 = n by FACIRC_2:37;
deffunc H₄( Nat) -> Element of NAT = N . $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 -BitGFA0Str f,g) = $1 -BitGFA0CarryOutput 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 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
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 13;
then A9: x = H₅(n) by A6, A8;
then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2 ] by Lm2;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2 ] by A9, Lm2;
hence ( not A = H₂(x,n) or for s being State of A holds Following s,H₄(1) is stable ) by A2, A10, GFACIRC1:48; :: thesis:

end;

set Sn = n -BitGFA0Str f,g;
set An = n -BitGFA0Circ f,g;
set o0 = 0 -BitGFA0CarryOutput f,g;
consider f1, g1, h1 being ManySortedSet of NAT such that
A11: n -BitGFA0Str f,g = f1 . n and
A12: n -BitGFA0Circ 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 of 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 Def2;

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

end;

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

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

end;

set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A25: x = h . n ; :: thesis:
n in NAT by ORDINAL1:def 13;
then A26: x = H₅(n) by A6, A25;
then A27: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2 ] by Lm2;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2 ] by A26, Lm2;
then A28: InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A27, GFACIRC1:41;
let a be pair set ; :: according to FACIRC_1:def 2 :: thesis:
assume A29: a in (InputVertices H₁(x,n)) \ {x} ; :: thesis:
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:

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 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A33: x = h . n ; :: thesis:
n in NAT by ORDINAL1:def 13;
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, Th7; :: thesis:
A35: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2 ] by A34, Lm2;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2 ] by A34, Lm2;
then InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A35, GFACIRC1:41;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis:
A36: InnerVertices H₁(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2 ]} \/ {(GFA0AdderOutput (f . (n + 1)),(g . (n + 1)),x)}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2 ],[<*(g . (n + 1)),x*>,and2 ],[<*x,(f . (n + 1))*>,and2 ]}) \/ {(GFA0CarryOutput (f . (n + 1)),(g . (n + 1)),x)} by GFACIRC1:39;
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;