set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
let n be Nat; :: thesis:
let x, y be FinSequence; :: thesis:
consider f, g, h being ManySortedSet of NAT such that
A1: n -BitGFA0Str (x,y) = f . n and
A2: n -BitGFA0Circ (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 +* (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) ) by Def2;
A7: n -BitGFA0CarryOutput (x,y) = h . n by A3, A4, A5, A6, Th1;
A8: (n + 1) -BitGFA0Str (x,y) = f . (n + 1) by A3, A4, A5, A6, Th1;
A9: (n + 1) -BitGFA0Circ (x,y) = g . (n + 1) by A3, A4, A5, A6, Th1;
(n + 1) -BitGFA0CarryOutput (x,y) = h . (n + 1) by A3, A4, A5, A6, Th1;
hence ( (n + 1) -BitGFA0Str (x,y) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ (x,y) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) ) by A1, A2, A6, A7, A8, A9; :: thesis: