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