Exercise 2: Proving power_of_two(n) Correctly Computes 2^n — Possible Solution
====================================================================

THE CLAIM
------------------------------
power_of_two(n) returns 2^n, for every n >= 0.

BASE CASE (n = 0)
------------------------------
Per the function's own definition, when n == 0, it returns 1
directly. And 2^0 = 1 by definition. The function's output matches
the claim exactly for n = 0. Base case holds.

INDUCTIVE STEP
------------------------------
Inductive hypothesis: assume, for an arbitrary k >= 0, that
power_of_two(k) correctly returns 2^k.

Goal: show that power_of_two(k+1) then correctly returns 2^(k+1).

Per the function's own definition, since k+1 != 0, calling
power_of_two(k+1) executes the recursive branch:

  power_of_two(k+1) = 2 * power_of_two(k)

By the inductive hypothesis, power_of_two(k) returns 2^k. Substituting
this in:

  power_of_two(k+1) = 2 * 2^k = 2^(k+1)

This is exactly the claim, for k+1. The inductive step is complete.

CONCLUSION
------------------------------
By the base case and the inductive step together, power_of_two(n)
correctly returns 2^n for every n >= 0. QED.

WHY THIS IS STRUCTURAL INDUCTION, PER THIS CHAPTER'S OWN TERMINOLOGY
------------------------------
The "size" being inducted on here is the value of n itself, which
also directly controls how many recursive calls the function makes
before reaching its base case. This is exactly the same pattern this
chapter's own sum_list worked example used, inducting on n instead of
list length - proving a recursive function correct by assuming
correctness at one smaller input and showing it's preserved at the
next.

WHY THE INDUCTIVE HYPOTHESIS IS WHAT ACTUALLY JUSTIFIES THE
SUBSTITUTION
------------------------------
The step "power_of_two(k) returns 2^k" is not something re-derived
from scratch during the inductive step - it's exactly the assumption
being granted as the inductive hypothesis. This is precisely why
induction can prove correctness for every possible n without having to
trace through every individual recursive call chain by hand.

WHY THIS WORKS AS AN ANSWER
------------------------------
It verifies the base case directly against the function's own defined
behavior, states the inductive hypothesis for an arbitrary k, and
uses the function's own recursive definition together with that
hypothesis to derive the exact claim for k+1.