Two's complement proof

Question

Is it possible to prove by induction that the two's complement of any string of 0's will always result in 0, for all sequences of length n?

I'm trying to do this using the value formula, i.e.

value = -a_n-1 x 2^(n-1) + summation{i=0 to n} (a_i x 2^i), where n = number of bits in string

Answer 1

Isn't the 2's complement of 111..111 just 1 (which means that 111..111 represents -1)?

Answer 2

Are you asking to prove that, for example, the two's complement of 1111 1111 is 0000 0000? If so, you can not prove it because it is false. The two's complement of 1111 1111 is 0000 0001.

    1111 1111
->  0000 0000 <- one's complement
->  0000 0001 <- add 1

Response to your edit: Sure. But you don't need induction. Inverting all of the bits of 0_n to obtain the one's complement gives you 1_n and adding 1 flips all the bits back to zero (1 + 1 = 10 and the carry bit percolates through to end where we drop it). QED.

Answer 3

1) Definition of two complement of X: flip the bits of X and sum 1

2) Binary sum of two variables with 1 bit (http://www.play-hookey.com/digital/adder.html) (being b1 the first variable and b2 the second variable. b1:X denote bit X in the variable)

r1 = b1:1 XOR b2:1
carry = b1:1 AND b2:1

2.1) if both bits are one b1:1 and b2:1

r1 = 0  (always)
carry = 1 (always)

3) Binary sum of two variables with 2 bit

r1 = b1:1 XOR b2:1 
carry1 = b1:1 AND b2:1

r2 = (b1:2 XOR b2:2) XOR carry:1
carry2 = (b1:2 AND b2:2) OR (b1:2 AND carry:1) OR (b2:2 AND carry:1)

3.1) From 2.1 we can reduce

carry2 = (b1:2 AND b2:2) OR (b1:2 AND 1) OR (b2:2 AND 1)
carry2 = b1:2 OR b2:2

4) Be a number Zero all zeros. Flipping all bits will generate an all ones number: Ones

5) Bit 0 XOR Anything = Anything (truth table of XOR)

6) Applying (1) on number Zero

6.1) flip

 Flipping Zero = Ones

6.2) sum 1

 result = Ones + N_One (N_One = 00...001)
 result:1 = 0 (from 2.1)
 carry:1 = 1 (from 2.1)

6.3) As all bits from N_One except N_One:1 are zero.

 result:n = (Ones:n XOR N_One:n) XOR carry:(n-1) (from 3)
 result:n = (Ones:n XOR 0) XOR carry:(n-1) (definition of N_One 6.2)
 result:n = Ones:n XOR carry:(n-1)

6.4) from 3.1

carry:n = Ones:n OR N_One:n -> if carry:n-1 is 1
carry:n = 1 OR 0            -> if carry:n-1 is 1
carry:n = 1                 -> if carry:n-1 is 1

As the first carry (carry:1) is defined as 1 from 6.1 all carries are defined as 1

7) from 6.3 and 6.4

 result:n = Ones:n XOR carry:(n-1)
 result:n = 1 XOR 1
 result:n = 0

For any value of n, proving that (~n+1) is always 0. (the last carry for a machine with fixed bitfield size is always ignored)

QED