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 ap, bm, cp, dm be FinSequence; :: thesis:
consider f, g, h being ManySortedSet of NAT such that
A1: n -BitFTA1Str (ap,bm,cp,dm) = f . n and
A2: n -BitFTA1Circ (ap,bm,cp,dm) = 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 +* (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) ) by Def9;
A7: n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n by A3, A4, A5, A6, Th12;
A8: (n + 1) -BitFTA1Str (ap,bm,cp,dm) = f . (n + 1) by A3, A4, A5, A6, Th12;
A9: (n + 1) -BitFTA1Circ (ap,bm,cp,dm) = g . (n + 1) by A3, A4, A5, A6, Th12;
(n + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) = h . (n + 1) by A3, A4, A5, A6, Th12;
hence ( (n + 1) -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Str (ap,bm,cp,dm)) +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Circ (ap,bm,cp,dm)) +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm))) ) by A1, A2, A6, A7, A8, A9; :: thesis: