Proof by induction that $x_{n} + by_{n} = a$

Question

I have an algorithm where a and b $\in$ Z+

MUL(a,b)
   x = a
   y = 0
WHILE x >= b DO
   x = x-b
   y = y+1
IF x = 0 THEN
   RETURN(y)
ELSE
   RETURN(-1)

I need to prove by induction that

$x_{n} + by_{n} = a$

is true if $x_{n}$ and $y_{n}$ are the values for x and y after n runs of the WHILE-loop.

My approach is to to prove that its true for the basecase where the WHILE-loop runs 0 times.

When the WHILE-loop runs 0 times (n = 0), we know that y = 0 since y is counting the amount of times the WHILE-loop is ran. So we have:

\begin{equation} \begin{split} x_{0} + by_{n} =& a \\ x_{0} + b*0 =& a \\ x_{0} =& a \\ \end{split} \end{equation}

If we input $a = 1$ og $b = 2$ into $MUL()$. The result will be be $y = 0$ and $x = 1 = a$.

I'm not sure if this basecase step is correct and I am not sure how to proceed from here. I know I need to prove if it's true for n + 1. But how I do it I don't know. I hope somebody can help me!

Answer 1

Strictly speaking, we do not know anything like "$y$ is counting the amount of times the WHILE loop is run" beforehand; however, this (i.e., $y_n=n$) may be a corollary of an analysis of the code.

After $0$ loops, i.e., immediately before entering the while loop, only x = a and y = 0 are executed, hence indeed $x_0=a$ and $y_0=0$. Thus

$$\tag1 x_n+by_n=a\qquad\text{and}\qquad y_n=n$$

holds for the base case $n=0$

Assume $x_n+by_n=a$ and $y_n=n$ after $n$ loops. Then in the next loop, the statements x = x - b and y = y + 1 are executed. It follows that $x_{n+1}=x_n-b$ and $y_{n+1}=y_n+1$. Therefore, using the induction hypothesis, $$x_{n+1}+by_{n+1}=x_n-b+b(y_n+1)=x_n+by_n=a $$ and $$y_{n+1}=x_n+1=n+1,$$ i.e., $(1)$ with $n\leftarrow n+1$. Therefore we have shows that $(1)$ holds for all $n\in\Bbb N_0$.

---

Once this is shown, we see from $(1)$ that $$x_n=a-by_n=a-bn. $$ So for $n$ large enough, $x_n\ge b$ will not hold, and the WHILE loop will terminate. Let $n$ be minimal with $x_n<b$. Then the return value of MUL will be $y_n$ if $x_n=0$, and $-1$ otherwise. As $x_n=0$ implies $by_n=a$, we conclude that for $a,b\in \Bbb Z^+$, $$\text{MUL}(a,b)=\begin{cases}\frac ab&\text{if }b\text{ divides }a\\-1&\text{otherwise}\end{cases} $$