Induction proof of alpha-beta search

Is there a functional specification of alpha-beta search that makes it easy to prove by induction that the algorithm works?

The following is an easy to understand approach to tree pruning. It's easy to see why it's correct.

Let's start with ordinary minimax evaluation. If you are trying to evaluate position $p$ when it's the minimizing player's turn, you return $\min\{\operatorname{eval}(p',\text{max}) \mid p'\text{ successor of }p\}$.

To do tree pruning you change what $\operatorname{eval}(p',\text{max})$ does. Instead of returning a single value, it streams messages to you. Messages like "my final value will be at greater than 3", "my value will be greater than 20", "my value is 23". If the minimizer already got a message saying that one successor $p'$ has has value $5$, and it gets a message from $\text{eval}(p'',\text{max})$ saying that its value will be at least $10$ then the minimizer will close the channel with $\text{eval}(p'',\text{max})$.

It's easy to translate this into code and it's clear that it's functionally identical to minimax.

But it's not quite the algorithm presented on Wikipedia under alpha beta pruning.

StackExchange Computer Science Q#48724, answer score: 2