Consider the following recursive algorithm intended to find the greatest common divisor of nonnegative integers a and b with a < b.

procedure gcd(a, b : nonnegative integers with a < b)

if a=0 then return b

else return gcd( b mod a, a )

end.

Prove that any sequence of recursive calls terminates in a base case. (Note that b mod a is the remainder when b is divided by a.)