let n be Nat; :: thesis: for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitGFA0Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable
let f, g be nonpair-yielding FinSeqLen of n; :: thesis: for s being State of (n -BitGFA0Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable
deffunc H₁( set , Nat) -> ManySortedSign = BitGFA0Str ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₂( set , Nat) -> MSAlgebra over 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)];
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) ;

A5: now :: thesis: for s being State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) holds Following (s,H₄( 0 )) is stable

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₅( 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

proof

set f1 = and2 ;
set f0 = xor2 ;
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 A8: 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 12;
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:40; :: thesis: verum

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 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 Def2;

now :: thesis: for i being object st i in NAT holds
h1 . i = h . i

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

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

proof

take f1 ; :: thesis: ex v being ManySortedSet of NAT st
( n -BitGFA0Str (f,g) = f1 . H₄(2) & n -BitGFA0Circ (f,g) = v . H₄(2) & f1 . 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 over S
for x being set
for A2 being non-empty MSAlgebra over 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 -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 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) ) ) )
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 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: verum

end;

A20: ( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is Relation & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is without_pairs ) by FACIRC_1:38, FACIRC_1:39;
A21: 0 -BitGFA0CarryOutput (f,g) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by Th2;
InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42;
then A22: ( h . 0 = 0 -BitGFA0CarryOutput (f,g) & 0 -BitGFA0CarryOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) ) by A6, A21, TARSKI:def 1;
A23: for n being Nat
for x being set holds InnerVertices H₁(x,n) is Relation by GFACIRC1:32;
A24: for n being Nat
for x being set st x = h . n holds
(InputVertices H₁(x,n)) \ {x} is without_pairs

proof

set f1 = and2 ;
set f0 = xor2 ;
let n be Nat; :: thesis: for x being set st x = h . n holds
(InputVertices H₁(x,n)) \ {x} is without_pairs
let x be set ; :: thesis: ( x = h . n implies (InputVertices H₁(x,n)) \ {x} is without_pairs )
assume A25: x = h . n ; :: thesis: (InputVertices H₁(x,n)) \ {x} is without_pairs
n in NAT by ORDINAL1:def 12;
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:33;
let a be pair object ; :: according to FACIRC_1:def 2 :: thesis: not a in (InputVertices H₁(x,n)) \ {x}
assume A29: a in (InputVertices H₁(x,n)) \ {x} ; :: thesis: contradiction
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: verum

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

proof

set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
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 A33: 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 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, Th7; :: thesis: ( x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )
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:33;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis: H₃(x,n) in InnerVertices H₁(x,n)
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:31;
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: verum

end;

for s being State of (n -BitGFA0Circ (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 -BitGFA0Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; :: thesis: verum