let x, y be FinSequence; for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n )
let f, g, h be ManySortedSet of NAT ; ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) implies for n being Nat holds
( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n ) )
set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2));
deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3));
deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H4( Nat, set ) -> Element of InnerVertices (GFA0CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA0CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
assume that
A1:
( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) )
and
A2:
h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A3:
for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = H1(S,z,n) & g . (n + 1) = H2(S,A,z,n) & h . (n + 1) = H3(z,n) )
; for n being Nat holds
( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n )
let n be Nat; ( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n )
consider f1, g1, h1 being ManySortedSet of NAT such that
A4:
n -BitGFA0Str (x,y) = f1 . n
and
A5:
n -BitGFA0Circ (x,y) = g1 . n
and
A6:
f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A7:
g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A8:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A9:
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) = H1(S,z,n) & g1 . (n + 1) = H2(S,A,z,n) & h1 . (n + 1) = H3(z,n) )
by Def2;
A10:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . 0 & A = g . 0 )
by A1;
A11:
( f . 0 = f1 . 0 & g . 0 = g1 . 0 & h . 0 = h1 . 0 )
by A1, A2, A6, A7, A8;
A12:
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set
for n being Nat holds H2(S,A,z,n) is non-empty MSAlgebra over H1(S,z,n)
;
( f = f1 & g = g1 & h = h1 )
from CIRCCMB2:sch 14(A10, A11, A3, A9, A12);
hence
( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n )
by A4, A5; n -BitGFA0CarryOutput (x,y) = h . n
A13:
for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = h . n holds
( f . (n + 1) = H1(S,z,n) & h . (n + 1) = H3(z,n) )
from CIRCCMB2:sch 15(A1, A3, A12);
A14:
f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
by A1;
A15:
for n being Nat
for z being set st z = h . n holds
h . (n + 1) = H3(z,n)
from CIRCCMB2:sch 3(A14, A13);
A16:
dom h = NAT
by PARTFUN1:def 2;
A17:
h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
by A2;
A18:
for n being Nat holds h . (n + 1) = H4(n,h . n)
by A15;
consider h1 being ManySortedSet of NAT such that
A19:
n -BitGFA0CarryOutput (x,y) = h1 . n
and
A20:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
and
A21:
for n being Nat holds h1 . (n + 1) = H4(n,h1 . n)
by Def3;
A22:
dom h1 = NAT
by PARTFUN1:def 2;
A23:
h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
by A20;
A24:
for n being Nat holds h1 . (n + 1) = H4(n,h1 . n)
by A21;
h = h1
from NAT_1:sch 15(A16, A17, A18, A22, A23, A24);
hence
n -BitGFA0CarryOutput (x,y) = h . n
by A19; verum