Since and must add add to zero in a fixed-width binary adder, it must be the case that

(where represents fixed-width addition) or, equivalently,

The logical ``not'' function can be written as for a single bit and is defined by

for a bit vector. Since (for representable *x*)

it is easy to verify the well-known formula

Mon Dec 11 17:02:42 CST 2000