# iterate algorithm/program correctness proof by induction

Suppose I have a function where it calculates which bit is larger called LargerBinary.

Let's say I have an input 110111;101001, the output will be 110111 and if the input is 110110:110110, the output will be 110110.

Inside of LargerBinary function, I would have sub function called SmallerBinary, which it calculates each bit of input, and this function will return true if and only if x1(first) one is smaller than the x2(second) one and it will return false if and only if x1 is larger than the x2.

Here is LargerBinary:

LargerBinary(a1,a2...an;b1,b2...bn:two binary number with n bits)

for i:=1 to n
if SmallerBinary(ai,bi) then
return b1,b2,...,bi
if SmallerBinary(bi,ai) then
return a1,a2,...,ai
return a1,a2,...,ai


how would you prove by induction if the loop invariant is given:

After k iteration of the for loop, if the algorithm has not yet terminated, we know a1,a2,...,ak = b1,b2,...,bk.

I know for base case k=1, I need to prove that it holds when k =1 How would you proove for the base case?

and I also need to proof that it holds for every k (for k-1)

What would be Induction hypothesis and the induction step? I am a bit confused on this question. Thanks in advance

The base case. For $k=1$, if the algorithm has not yet terminated, then we know that we did not enter to either the first if nor the second if, otherwise the algorithm would have had terminated already. Thus, $a1=b1$. This is proves the base case.
Suppose that: After $k$ iterations, if the algorithm has not yet terminated, we know that $a1a2\ldots ak=b1b2\ldots bk$. Prove that: After $k+1$ iterations, if the algorithm has not yet terminated, we know that $a1a2\ldots akak+1=b1b2\ldots bkbk+1$.
Well, we know that, by the induction hypothesis that, the algorithm has not yet terminated after the iteration $k$ and $a1a2\ldots ak=b1b2\ldots bk$. If the algorithm has not yet terminated after the iteration $k+1$, this means that we did not enter to either the first if nor the second if. Then, We have that $ak+1=bk+1$. Finally, $a1a2\ldots akak+1=b1b2\ldots bkbk+1$. This proves the claim.