Quote from: dentldir on August 02, 2013, 06:25:15 AM

Clever implementation. Lends itself well to complete regression testing / provability.

On first inspection, I'm not convinced that the reduced form is correct. By definition, doesn't c31 depend on a30 if b30 = 1?

Looking at it another way, the third term of c31 will be zero in all but 2 out of 2^32 cases for all possible values of b and in all cases if a0 = 0.

Thank you dentldir, it turns out there was a bug in the module feeding stuff to wolfram,

new bits for (c = a + b) are looking like this:

c0: (a0^b0)
c1: (a1^a0&b0^b1)
c2: (a2^a1&b1^a0&b0&(a1^b1)^b2)
c3: (a3^a2&b2^a1&b1&(a2^b2)^a0&b0&(a1^b1)&(a2^b2)^b3)
c4: (a4^a2&a3&b2^a3&b3^a2&b2&b3^a1&b1&(a2^b2)&(a3^b3)^a0&b0&(a1^b1)&(a2^b2)&(a3^b3)^b4)
c5: (a5^a4&(a3&b3^a2&b2&(a3^b3))^(a4^a3&b3^a2&b2&(a3^b3))&b4^a1&b1&(a2^b2)&(a3^b3)&(a4^b4)^a0&b0&(a1^b1)&(a2^b2)&(a3^b3)&(a4^b4)^b5)
c6: (a6^a4&a5&(a3&b3^a2&b2&(a3^b3))^a5&(a4^a3&b3^a2&b2&(a3^b3))&b4^(a5^a4&b4^a3&b3&(a4^b4)^a2&b2&(a3^b3)&(a4^b4))&b5^a1&b1&(a2^b2)&(a3^b3)&(a4^b4)&(a5^b5)^a0&b0&(a1^b1)&(a2^b2)&(a3^b3)&(a4^b4)&(a5^b5)^b6)

at first glance they verified in an excel sheet, other bits are still simplifying.