Why Does It Work? [Step 2]

• 1. Initially x y +z = a b.
• 2. Inductive Step
  • Let x, y, z be values at the top of the loop.
  • Assume x y + z = a b holds.
  • Let x', y', z' be the values after the loop.
  • If x is odd:
    • x' = (x-1)/2
    • y' = 2 y
    • z' = z + y
    • x' y' + z' = (x-1)/2 (2 y) + z + y
      = (x-1) y + z + y = x y - y + z + y = x y + z = a b
  • if x is even:
    • x' = x/2
    • y' = 2 y
    • z' = z
    • x' y' + z' = (x/2) (2 y) + z = x y + z = a b
  • Therefore x'y'+z' = ab.
• 3. Variable x starts at at least one and decreases on each iteration down to zero. Therefore, algorithm terminates.
• 4. At termination, x y + z = a b, but x = 0, so z = a b.