agl/critbit — Issue #1: 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"
Author: nolanw
Created: 2011-12-04 07:57:48+00:00
State: open

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.)