let ap, bm, cp, dm be FinSequence; :: thesis: 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n & n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n )
let f, g, h be ManySortedSet of NAT ; :: thesis: ( 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 +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & g . (n + 1) = A +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z)) & h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),z) ) ) implies for n being Nat holds
( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n & n -BitFTA1CarryOutput (ap,bm,cp,dm) = 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 H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitFTA1Str ((ap . ($3 + 1)),(bm . ($3 + 1)),(cp . ($3 + 1)),(dm . ($3 + 1)),$2));
deffunc H₂( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitFTA1Str ((ap . ($4 + 1)),(bm . ($4 + 1)),(cp . ($4 + 1)),(dm . ($4 + 1)),$3)) = $2 +* (BitFTA1Circ ((ap . ($4 + 1)),(bm . ($4 + 1)),(cp . ($4 + 1)),(dm . ($4 + 1)),$3));
deffunc H₃( set , Nat) -> Element of InnerVertices (BitFTA1Str ((ap . ($2 + 1)),(bm . ($2 + 1)),(cp . ($2 + 1)),(dm . ($2 + 1)),$1)) = BitFTA1CarryOutput ((ap . ($2 + 1)),(bm . ($2 + 1)),(cp . ($2 + 1)),(dm . ($2 + 1)),$1);
deffunc H₄( Nat, set ) -> Element of InnerVertices (BitFTA1Str ((ap . ($1 + 1)),(bm . ($1 + 1)),(cp . ($1 + 1)),(dm . ($1 + 1)),$2)) = BitFTA1CarryOutput ((ap . ($1 + 1)),(bm . ($1 + 1)),(cp . ($1 + 1)),(dm . ($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) = H₁(S,z,n) & g . (n + 1) = H₂(S,A,z,n) & h . (n + 1) = H₃(z,n) ) ; :: thesis: for n being Nat holds
( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n & n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n )
let n be Nat; :: thesis: ( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n & n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n )
consider f1, g1, h1 being ManySortedSet of NAT such that
A4: n -BitFTA1Str (ap,bm,cp,dm) = f1 . n and
A5: n -BitFTA1Circ (ap,bm,cp,dm) = 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) = H₁(S,z,n) & g1 . (n + 1) = H₂(S,A,z,n) & h1 . (n + 1) = H₃(z,n) ) by Def9;
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 H₂(S,A,z,n) is non-empty MSAlgebra over H₁(S,z,n) ;
( f = f1 & g = g1 & h = h1 ) from CIRCCMB2:sch 14(A10, A11, A3, A9, A12);
hence ( n -BitFTA1Str (ap,bm,cp,dm) = f . n & n -BitFTA1Circ (ap,bm,cp,dm) = g . n ) by A4, A5; :: thesis: n -BitFTA1CarryOutput (ap,bm,cp,dm) = 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) = H₁(S,z,n) & h . (n + 1) = H₃(z,n) ) from CIRCCMB2:sch 15(A1, A3, A12);
A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1;
A15: dom h = NAT by PARTFUN1:def 2;
A16: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A2;
for n being Nat
for z being set st z = h . n holds
h . (n + 1) = H₃(z,n) from CIRCCMB2:sch 3(A14, A13);
then A17: for n being Nat holds h . (n + 1) = H₄(n,h . n) ;
consider h1 being ManySortedSet of NAT such that
A18: n -BitFTA1CarryOutput (ap,bm,cp,dm) = h1 . n and
A19: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A20: for n being Nat holds h1 . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h1 . n)) by Def10;
A21: dom h1 = NAT by PARTFUN1:def 2;
A22: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A19;
A23: for n being Nat holds h1 . (n + 1) = H₄(n,h1 . n) by A20;
h = h1 from NAT_1:sch 15(A15, A16, A17, A21, A22, A23);
hence n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n by A18; :: thesis: verum