Incomplete proof that "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two"

[nolanw]

I'm curious about the proof you give, in section 12, for the statement "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two". It seems incomplete to me.

You divide the number's bits up WLOG into three pieces: a (possibly empty) series of zeros, followed by a one, followed by a series ones and zeros. The number 1 (i.e. 0x01) cannot be split as such.

1 is of course a power of two, and the most-significant 1 is maintained as a result of the described operations, so I think all you need to do is point out that the third series of bits may also be empty.

(P.S. Thanks for the awesome explanation, I was kind of lost with djb's relatively terse description.)

[agl]

On Sun, Dec 4, 2011 at 2:57 AM, Nolan Waite
[email protected]
wrote:

I'm curious about the proof you give, in section 12, for the statement "the only non-zero values for which the sets of true bits for x and x − 1 are disjoint, are powers of two". It seems incomplete to me.

You're absolutely right, thanks for that.

I don't have cweb installed at the moment, so I haven't updated the
PDF. But I've fixed the .w file and it'll get included the next time
that I do so.

Cheers

AGL

Adam Langley [email protected] http://www.imperialviolet.org