# Prove grade-school multiplication algorithm applied to binary numbers

I want to prove that the basic multiplication algorithm is correct when applied to binary numbers. I try to follow the steps described here and here but didn't succeed.

The basic implementation algorithm is the multiply function defined below, the other functions are given by completeness (this is F# but it reads as pseudo code):

let toBitsArray (x : int) =
let bitArray = System.Collections.BitArray(System.BitConverter.GetBytes(x))
let bits = Array.zeroCreate<bool> bitArray.Count
bitArray.CopyTo(bits, 0)
bits

(* Gives an array of bits (bool: 1 or 0) in little endian representation
for example 5 = 00000000000000000000000000000101 (32 bits)
the function will give this array:
[|true; false; true; false; false; false; false; false; false; false;
false; false; false; false; false; false; false; false; false;
false; false; false; false; false; false; false; false; false;
false; false; false; false|]
which represents 10100000000000000000000000000000 (32 bits) *)
let toLittleEndianBitsArray (x : int) =
let bits = toBitsArray x
if System.BitConverter.IsLittleEndian
then bits
else Array.rev bits

let multiply (x : int) (y : int) =
let by = toLittleEndianBitsArray y
let rec loop (x : int64) (y : bool list) =
if List.isEmpty y
then 0L
else

• well, I'm not being able of coming with an induction step that eases the proof, in the examples I linked there is P(m) = x+y=m+1, m >= 2 and x, y >= 1 then it proves the recursion with multiplication(x-1,y) but I have to prove it with multiplication( leftshift x, y)... I do not see how to proceed Nov 26 '19 at 22:39