let n be Nat; :: thesis:
let p, q be FinSeqLen of n; :: thesis:
let p1, p2, q1, q2 be FinSequence; :: thesis:
set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)];
set Sn1 = n -BitGFA1Str ((p ^ p1),(q ^ q1));
set An1 = n -BitGFA1Circ ((p ^ p1),(q ^ q1));
set On1 = n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1));
deffunc H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2));
deffunc H₂( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3));
deffunc H₃( set , Nat) -> Element of InnerVertices (GFA1CarryStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = GFA1CarryOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1);
deffunc H₄( Nat, set ) -> Element of InnerVertices (GFA1CarryStr (((p ^ p1) . ($1 + 1)),((q ^ q1) . ($1 + 1)),$2)) = GFA1CarryOutput (((p ^ p1) . ($1 + 1)),((q ^ q1) . ($1 + 1)),$2);
consider f1, g1, h1 being ManySortedSet of NAT such that
A1: n -BitGFA1Str ((p ^ p1),(q ^ q1)) = f1 . n and
A2: n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = g1 . n and
A3: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A4: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A5: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: 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) = H₁(S,z,n) & g1 . (n + 1) = H₂(S,A,z,n) & h1 . (n + 1) = H₃(z,n) ) by Def6;
set Sn2 = n -BitGFA1Str ((p ^ p2),(q ^ q2));
set An2 = n -BitGFA1Circ ((p ^ p2),(q ^ q2));
set On2 = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2));
deffunc H₅( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str (((p ^ p2) . ($3 + 1)),((q ^ q2) . ($3 + 1)),$2));
deffunc H₆( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3));
deffunc H₇( set , Nat) -> Element of InnerVertices (GFA1CarryStr (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1)) = GFA1CarryOutput (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1);
deffunc H₈( Nat, set ) -> Element of InnerVertices (GFA1CarryStr (((p ^ p2) . ($1 + 1)),((q ^ q2) . ($1 + 1)),$2)) = GFA1CarryOutput (((p ^ p2) . ($1 + 1)),((q ^ q2) . ($1 + 1)),$2);
consider f2, g2, h2 being ManySortedSet of NAT such that
A7: n -BitGFA1Str ((p ^ p2),(q ^ q2)) = f2 . n and
A8: n -BitGFA1Circ ((p ^ p2),(q ^ q2)) = g2 . n and
A9: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A10: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A12: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f2 . n & A = g2 . n & z = h2 . n holds
( f2 . (n + 1) = H₅(S,z,n) & g2 . (n + 1) = H₆(S,A,z,n) & h2 . (n + 1) = H₇(z,n) ) by Def6;
defpred S₁[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) );
A13: S₁[ 0 ] by A3, A4, A5, A9, A10, A11;
A14: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume that
A15: ( i <= n implies ( h1 . i = h2 . i & f1 . i = f2 . i & g1 . i = g2 . i ) ) and
A16: i + 1 <= n ; :: thesis:
A17: len p = n by CARD_1:def 7;
A18: len q = n by CARD_1:def 7;
A19: dom p = Seg n by A17, FINSEQ_1:def 3;
A20: dom q = Seg n by A18, FINSEQ_1:def 3;
0 + 1 <= i + 1 by XREAL_1:6;
then A21: i + 1 in Seg n by A16, FINSEQ_1:1;
then A22: (p ^ p1) . (i + 1) = p . (i + 1) by A19, FINSEQ_1:def 7;
A23: (p ^ p2) . (i + 1) = p . (i + 1) by A19, A21, FINSEQ_1:def 7;
A24: (q ^ q1) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def 7;
A25: (q ^ q2) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def 7;
defpred S₂[ set , set , set , set ] means verum;
A26: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f1 . 0 & A = g1 . 0 & x = h1 . 0 & S₂[S,A,x, 0 ] ) by A3, A4;
A27: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . n & A = g1 . n & x = h1 . n & S₂[S,A,x,n] holds
S₂[H₁(S,x,n),H₂(S,A,x,n),H₃(x,n),n + 1] ;
A28: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H₂(S,A,x,n) is non-empty MSAlgebra over H₁(S,x,n) ;
for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . n & A = g1 . n & S₂[S,A,h1 . n,n] ) from CIRCCMB2:sch 13(A26, A6, A27, A28);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A29: S = f1 . i and
A30: A = g1 . i ;
thus h1 . (i + 1) = H₇(h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= h2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; :: thesis:
thus f1 . (i + 1) = H₅(S,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= f2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; :: thesis:
thus g1 . (i + 1) = H₆(S,A,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13
.= g2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; :: thesis:

end;

A31: for i being Nat holds S₁[i] from NAT_1:sch 2(A13, A14);
hence ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) ) by A1, A2, A7, A8; :: thesis:
A32: n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = h1 . n by A3, A4, A5, A6, Th15;
n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) = h2 . n by A9, A10, A11, A12, Th15;
hence n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) by A31, A32; :: thesis: