How can I prove the correctness of this exponentiation algorithm using induction?

Question

I have the following algorithm. How could I prove it using induction that for every $n\ge 0$, Exp(n)${}= 2 ^ n$?

Exp(n)
    If n = 0
        Return 1
    
    If n is even
        temp = Exp(n/2)
        Return temp × temp
    Else
        temp = Exp((n−1)/2)
        Return temp × temp × 2

Answer 1

$Exp(0) = 1 = 2^0$ is trivially correct (hard coded) by the algorithm.

Assume the algorithm holds for values of $n$ up to $k$. Now consider the algorithm for input $n = k+1$. We compute $Exp(n) = Exp(k+1)$ using the algorithm:

In the case that $n = k+1$ is even:

The algorithm computes $temp = Exp(\frac{k+1}{2})$. After this step $temp$ holds the correct value for $2^{\frac{k+1}{2}}$ because we assumed the algorithm is correct for values up to $k$ [1]. The algorithm correctly returns $temp*temp = 2^{\frac{k+1}{2}}*2^{\frac{k+1}{2}} = 2^{k+1}$.

In the case that $n = k+1$ is uneven:

The algorithm computes $temp = Exp(\frac{n-1}{2}) = Exp(\frac{k+1-1}{2}) = Exp(\frac{k}{2})$. After this step $temp$ holds the correct value for $2^{\frac{k}{2}}$ because we assumed the algorithm is correct for values up to $k$ [1]. The algorithm correctly returns $temp*temp*2 = 2^{\frac{k}{2}}*2^{\frac{k}{2}}*2 = 2^{k+1}$.

i.e. since $Exp(0) = 1$ is trivially correct by the algorithm and we showed that the algorithm is correct for $Exp(n+1)$ if $Exp(n)$ is correct; it follows that the algorithm is correct for every $n \geq 0$.

[1] Technically you also have to show that $\frac{k+1}{2} \leq k$ and $\frac{k}{2} \leq k$ for every $k > 0$ but that seems easy enough to prove.