Correctness with/without induction I am a developer who tries to improve himself in algorithm design fields, and I got stuck in a problem. The mission is to prove the correctness of the following algorithm:
For all integer constants c>=2:
function multiple(y, z)
    // comment: Return the product yz
    if (z == 0) return 0;
    return multiple(c*y, floor(z / c)) + y * (z % c);

Now what I got is for cases:
1. z == c => c * y * (1 % c) => z * y * 1
2. z < c  => y * (z % c) => y * z

I got stuck when z > c. I couldn't find a general calculation for this state (I followed the recursion for some cases, but it didn't get me any closer to the general case).
[The question taken from The Algorithm Design Manual - second edition, by Steven S. Skiena]
Thanks for any help.
 A: Let $z=qc+r$
$\lfloor \frac{z}{c} \rfloor=q$,
$z\equiv r \pmod c$
Given $2$ integers $y,z$ the algorithm in order to compute $M(y,z)$ computes the following
$$M(cy,q)  + ry$$
which is true since $z=qc+r$ and $yz=qyc+ry$
Another way to look at this is,
Lets say there are $2$ numbers $17$ and $15$
In order to compute $M(17,15)$ , the algorithm breaks $15$, which is your $z$ in to smaller parts namely a multiple of $c$ and a leftover part which would be $z\equiv r \pmod c$ in this case.
Now, each product can be found separately, the algorithm continues to break up the multiplication into even smaller steps.
A: For this you want to use strong induction.  That is, you want to prove $f(p, q) = p \cdot q$ given the assumptions that $\forall r < q : f(p, r) = p \cdot r$
Because this isn't regular induction, your two cases aren't going to be "base case" and "inductive case".  You'll instead use the definition of $f$ to turn $f(p, q) = p \cdot q$ into the two algorithmic cases, $q = 0$ and $q \ne 0$.
So you need to prove $$\forall r < q : f(p, r) = p \cdot r \vdash f(p, 0) = p \cdot 0$$
and
$$\forall r < q : f(p, r) = p \cdot r \vdash f\left(c\cdot p, \left\lfloor \frac q c \right\rfloor\right) + p \cdot (q ~\%~ c) = p \cdot q$$
The first case is straightforward.  For the second case, use the inductive assumption to turn $f\left(c\cdot p, \left\lfloor \frac q c \right\rfloor\right)$ into a multiplication (because $\left\lfloor \frac q c \right\rfloor < q$) and use the theorem $a = \left \lfloor \frac ab \right \rfloor \cdot b + (a ~\% ~b)$.
