On Izumi's theorem on comparison of valuations

We prove that the sequence of MacLane key polynomials constructed in \cite{Mac1} and \cite{Sp2} for a valuation extension $(K,\nu)\subset (K(x),\mu)$ is finite, provided that both $\nu$ and $\mu$ are divisorial and $\mu$ is centered over an analytically irreducible local domain $(R,\frak{m})\subset K[x]$. As a corollary, we prove Izumi's theorem on comparison of divisorial valuations. %We show that the existence of Izumi constants is equivalent to the finiteness of the sequence of the MacLane key-polynomials. We give explicit bounds for the Izumi constant in terms of the key polynomials of the valuations. We show that this bound can be attained in some cases.