StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>1) Definition of two complement of X: flip the bits of X and sum 1</p> <p>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)</p> <pre><code>r1 = b1:1 XOR b2:1 carry = b1:1 AND b2:1 </code></pre> <p>2.1) if both bits are one b1:1 and b2:1</p> <pre><code>r1 = 0 (always) carry = 1 (always) </code></pre> <p>3) Binary sum of two variables with 2 bit</p> <pre><code>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) </code></pre> <p>3.1) From 2.1 we can reduce</p> <pre><code>carry2 = (b1:2 AND b2:2) OR (b1:2 AND 1) OR (b2:2 AND 1) carry2 = b1:2 OR b2:2 </code></pre> <p>4) Be a number Zero all zeros. Flipping all bits will generate an all ones number: Ones</p> <p>5) Bit 0 XOR Anything = Anything (truth table of XOR)</p> <p>6) Applying (1) on number Zero</p> <p>6.1) flip</p> <pre><code> Flipping Zero = Ones </code></pre> <p>6.2) sum 1</p> <pre><code> result = Ones + N_One (N_One = 00...001) result:1 = 0 (from 2.1) carry:1 = 1 (from 2.1) </code></pre> <p>6.3) As all bits from N_One except N_One:1 are zero.</p> <pre><code> 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) </code></pre> <p>6.4) from 3.1</p> <pre><code>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 </code></pre> <p>As the first carry (carry:1) is defined as 1 from 6.1 all carries are defined as 1</p> <p>7) from 6.3 and 6.4</p> <pre><code> result:n = Ones:n XOR carry:(n-1) result:n = 1 XOR 1 result:n = 0 </code></pre> <p>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)</p> <p>QED</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload