let n be Nat; :: thesis: for x, y being nonpair-yielding FinSeqLen of
for s being State of (n -BitGFA1Circ 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 -BitGFA1Circ f,g) holds Following s,(1 + (2 * n)) is stable
deffunc H₁( set , Nat) -> ManySortedSign = BitGFA1Str (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₂( set , Nat) -> MSAlgebra of 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 )];
n in NAT by ORDINAL1:def 13;
then consider N being Function of NAT ,NAT such that
A1: ( N . 0 = 1 & N . 1 = 2 & N . 2 = n ) by FACIRC_2:37;
deffunc H₄( 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 ) --> TRUE )); :: 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₅( Nat) -> Element of InnerVertices ($1 -BitGFA1Str f,g) = $1 -BitGFA1CarryOutput 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

set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f0 = xor2c ;
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 )
assume Z: x = h . n ; :: thesis: ( not A = H₂(x,n) or for s being State of A holds Following s,H₄(1) is stable )
n in NAT by ORDINAL1:def 13;
then x = H₅(n) by A4, Z;
then ( f . (n + 1) <> [<*(g . (n + 1)),x*>,and2a ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,and2 ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c ] ) by Lm4;
hence ( not A = H₂(x,n) or for s being State of A holds Following s,H₄(1) is stable ) by A1, GFACIRC1:85; :: thesis: verum

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 such that
A6: ( n -BitGFA1Str f,g = f1 . n & n -BitGFA1Circ f,g = g1 . n ) and
A7: ( f1 . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g1 . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h1 . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( 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 Def6;

now

let i be set ; :: thesis: ( i in NAT implies h1 . i = h . i )
assume Z: i in NAT ; :: thesis: h1 . i = h . i
then reconsider j = i as Nat ;
thus h1 . i = H₅(j) by A7, Th15
.= h . i by A4, Z ; :: thesis: verum

end;

then A8: h1 = h by PBOOLE:3;
A9: ex u, v being ManySortedSet of 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 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 -BitGFA1Str f,g = f1 . H₄(2) & n -BitGFA1Circ f,g = v . H₄(2) & f1 . 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 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 -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 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 -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 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 ) --> TRUE )) is Relation & not InputVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) is with_pair ) by FACIRC_1:38, FACIRC_1:39;
( 0 -BitGFA1CarryOutput f,g = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) = {[<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )]} ) by Th16, CIRCCOMB:49;
then A11: ( h . 0 = 0 -BitGFA1CarryOutput f,g & 0 -BitGFA1CarryOutput f,g in InnerVertices (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) ) by A4, TARSKI:def 1;
A12: for n being Nat
for x being set holds InnerVertices H₁(x,n) is Relation by GFACIRC1:77;
A13: for n being Nat
for x being set st x = h . n holds
not (InputVertices H₁(x,n)) \ {x} is with_pair

proof

set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f0 = xor2c ;
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
n in NAT by ORDINAL1:def 13;
then x = H₅(n) by A4, A14;
then ( f . (n + 1) <> [<*(g . (n + 1)),x*>,and2a ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,and2 ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c ] ) by Lm4;
then A15: InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by GFACIRC1:78;
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

set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f0 = xor2c ;
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) )
n in NAT by ORDINAL1:def 13;
then A18: ( x = H₅(n) & h . (n + 1) = H₅(n + 1) ) by A4, A17;
hence h . (n + 1) = H₃(x,n) by Th21; :: thesis: ( x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )
( f . (n + 1) <> [<*(g . (n + 1)),x*>,and2a ] & g . (n + 1) <> [<*x,(f . (n + 1))*>,and2 ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c ] ) by A18, Lm4;
then InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by GFACIRC1:78;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis: H₃(x,n) in InnerVertices H₁(x,n)
A19: 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:76;
H₃(x,n) in {H₃(x,n)} by TARSKI:def 1;
hence H₃(x,n) in InnerVertices H₁(x,n) by A19, XBOOLE_0:def 3; :: thesis: verum

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(A2, A3, A5, A9, A10, A11, A12, A13, A16);
hence for s being State of (n -BitGFA1Circ f,g) holds Following s,(1 + (2 * n)) is stable by A1; :: thesis: verum