Finiteness of GCD

Question

Binary GCD algorithm is described in the following link: https://en.wikipedia.org/wiki/Binary_GCD_algorithm

I wonder if there exists any mathematics proof of the finiteness of this algorithm,that is,how to prove that the GCD can be achieved within finite times of iterations with this algorithm?

while n != 0 and m != 0 do
    if n is even and m is even then
        ans ← ans × 2
        n ← n/2
        m ← m/2
    else if n is even and m is odd then
        n ← n/2
    else if n is odd and m is even then
        m ← m/2
    end if
    if n > m then
        swap(n, m)
    end if
    m ← (m − n)
end while
return n × ans

My partial solution:

set a>=b
case 1:a%2=0 and b%2=0 a=a/2-b/2;b=b/2;
case 2:a%2=0 and b%2=1 
    if a/2>=b a=a/2-b;b=b;
    else a=b b=b-a/2
case 3:a%2=1 and b%2=0 a=a-b/2;b=b/2;
case 4:a%2=1 and b%2=1 a=a-b;b=b

Since in every iteration,if a!=b,the larger one will strictly decrease.The ways to terminate the loop is that a=2b or a=b,both ways will let the larger one to turn zero.So the larger one will eventually the turn zero in finite times,and the loop stops.Can anybody give me advice on my proof?