let n be Nat; :: thesis:
let x, y be FinSequence; :: thesis:
set c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
consider f, g, h being ManySortedSet of NAT such that
A1: n -BitAdderStr (x,y) = f . n and
A2: n -BitAdderCirc (x,y) = g . n and
A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] 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 = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) by Def4;
A7: n -BitMajorityOutput (x,y) = h . n by A3, A4, A5, A6, Th6;
A8: (n + 1) -BitAdderStr (x,y) = f . (n + 1) by A3, A4, A5, A6, Th6;
A9: (n + 1) -BitAdderCirc (x,y) = g . (n + 1) by A3, A4, A5, A6, Th6;
(n + 1) -BitMajorityOutput (x,y) = h . (n + 1) by A3, A4, A5, A6, Th6;
hence ( (n + 1) -BitAdderStr (x,y) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc (x,y) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput (x,y) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))) ) by A1, A2, A6, A7, A8, A9; :: thesis: