Proof by induction for java algorithm

Question

double expRecursive(double x, int n) {
    if (n <= 4) {
        return expIterativ(x, n);
    }

    return expRecursive(x, n/2) *
           expRecursive(x, (n + 1)/2); }

Base Case: I checked that it works.

Inductive assumption: for n=p is: expRecursive($x,\frac{p}2$)×expRecursive($x,\frac {p+1}2)=x^p$

The proof, now I will show that it works for n=p+1:

expRecursive($x,\frac{p+1}2$)×expRecursive($x,\frac {p+2}2)= x^\frac{p+1}2 * x^\frac{p+2}2$

But obviously this doesn't equal to $x^{p+1}$, can someone help?

Answer 1

This is a little subtle, and it involves the semantics of the / operator, which rounds down.

If $n$ is even, then n / 2 evaluates to $\frac{n}{2}$, as does (n + 1)/2. So in this case, we use the strong inductive hypothesis to see that we are computing $(x^{\frac{n}{2}})^2 = x^n$.

Similarly, if $n$ is odd, then n / 2 evaluates to $\frac{n - 1}{2}$, while (n + 1)/2 evaluates to $\frac{n + 1}{2}$. So in this case, we use the strong inductive hypothesis to show we are computing $x^{\frac{n - 1}{2}} x^{\frac{n + 1}{2}} = x^n$, as required.