TADM2E 1.7
<h2>Base Case</h2>
The base case <math>(z = 0)</math> is true since it returns zero<br>
- <code>if <math>z = 0</math> then return(0)</code>
<h2>Assumptions</h2><br/> multiply(y,z) gives the correct answer where:
- z <= n
- c >= 2
- y >= 0<br />
<br /> We will also assume the following. A brief proof will follow:
- <math>\left \lfloor z / c \right \rfloor c + (z\,\bmod\,c) = z</math>
<br/>
<h2>Proof</h2><br /> Where z = n+1, c >= 2, y >= 0<br/> <br /> First we break the result of multiply into two parts:<br /> <br/> A = <math>multiply(cy, \left \lfloor [n+1]/c \right \rfloor)</math><br/> B = <math>y([n+1]\,\bmod\,c)</math><br/> <br/> <math>multiply(y,z) = A + B</math><br/> <br/> <br/> Now, because c >= 2 we know that <math>\left \lfloor (n+1) / c \right \rfloor < (n+1)</math>.<br /> Based on that, we know that the call to multiply in "A" returns the correct result.<br /> <br /> <math>A = multiply(cy, \left \lfloor [n+1]/c \right \rfloor) = cy * \left \lfloor [n+1] / c \right \rfloor</math><br /> <br /> So now let's transform A into something more useful:<br /> <br /> <math>A = cy * \left \lfloor [n+1] / c \right \rfloor = y * \left \lfloor z / c \right \rfloor c</math> <br/> (Note: We transformed n+1 back into z for simplicity)<br /> <br /> Based on our earlier assumption, we can transform this further:<br /> <br /> <math> \left \lfloor z / c \right \rfloor c + (z \,\bmod\, c) = z</math><br /> <math> \left \lfloor z / c \right \rfloor c = z - (z \,\bmod\, c)</math><br/> <br /> <math>A = y * \left \lfloor z / c \right \rfloor c = y (z - z \,\bmod\, c) = yz - y(z \,\bmod\, c)</math><br /> <br /> And now we add B back into the mix:<br /> <br /> <math>A + B = yz - y(z \,\bmod\, c) + y(z \,\bmod\, c) = yz</math><br /> <br /> <br/> <h2>Subproof</h2> <b>Show that <math>\left \lfloor z/c \right \rfloor c + z\,\bmod\,c = z</math> where c >= 2</b><br/> <br/> We can prove this statement using a general example.<br/> <br/> First, assume that <math>z\,\bmod\,c = a.</math><br/> <br/> Now, due to the definition of floor, we know the following:<br/> <br/> <math>(z-a) / c = \left \lfloor z / c \right \rfloor</math><br/> <br/> This is because the remainder can't possibly be taken into account during a "floor" operation.<br/> <br/> Based on that, we can restate the equation as:<br/> <br/> <math>(z-a) / c * c + a = (z - a) + a = z</math><br/> <br/>
