How to prove the outcome of both segment of code are equal?

Question

The main thing that I want to prove is that the outcome of both segments of code is the same.

Below is the code:

Segment A:

int A (int x, int y) {
  if (y==0) return x;
  return A(y, x % y);
}

Segment B:

int B (int x, int y) {
   while (y!=0) {
      int t = y;
      y = x % y;
      x = t;
   }
   return x;
}

$$%code from https://i.stack.imgur.com/oEGBo.png$$

Is it possible to prove equivalence using induction? If possible what would be the steps to proof A=B?

Answer 1

What would the inductive case look like?

Assume

$$\forall z ~:~ z < y \implies A(x, z) = B(x, z)$$ $$x = my + z $$ $$0 \le z < y$$

Prove

$$A(x, y) = B(x, y)$$

This is strong induction.