Proof of Brzozowski's algorithm for DFA minimization? Brzozowki's algorithm is cited widely.  Several questions here give examples or discuss its complexity. But I haven't been able to find a proof of correctness for the algorithm. How do we prove it correct?
Any proof accessible to CS undergraduates would be very welcome.
The proof of Brzozowski's result is technical, but not very complicated.
In fact we only have to consider one sequence of reversal-determinization, to obtain the minimality result we want. (The first sequence of reversal determination leads to a deterministic FSA for the reversal of the original language; the minimality proof is for the second reversal-determinization.)

First one needs some good view of the different automata involved. 
And nerves of steel.

The construction of Brzozowski.
Let $A = (Q, \Sigma, \delta, q_0, F)$ be a deterministic automaton for the language $L=L(A)$. We assume that all states of $Q$ are reachable from the initial state $q_0$.

In the first step one reverses the automaton: all edges are inverted, and inital and final states are swapped. Informally we get the automaton $\mathrm{rev}(A) = (Q, \Sigma, \delta^{-1}, F, q_0)$.

In the second step one determinizes the automaton so obtained, by the standard construction, but keeping only reachable states. We get $A'= \mathrm{det}(\mathrm{rev}(A)) = (Q', \Sigma, \delta', q'_0, F')$. 
The states of $A'$ are sets of states for $\mathrm{rev}(A)$: $Q'\subseteq 2^Q$; 
the initial state consists of the initial states for $\mathrm{rev}(A)$, which are final states in $Q$: $q'_0 = F$;
the final states in $A'$ are the states that contain a final state for $\mathrm{rev}(A)$: $U\in F'$ iff $q_0\in U$. 

The key of the proof is the following important relation between automata $A$ and $A'$.




  Basic Observation: $q\in \delta'(X,w^R)$ iff $\delta(q,w) \in X$.


Proof (one side only). $q\in \delta'(X,w^R)$ iff there exists a state $p$ in $X$ and a path from $p$ to $q$ in $\mathrm{rev}(A)$ with label $w^R$. But that means there is a path from $q$ to $p$ with label $w$ in $A$, or $\delta(q,w) = p$; thus $\delta(q,w) \in X$. end-of-proof.

As announced, this is used to prove the essential property we need.


  Property: $A'$ is minimal (and deterministic for $L^R$).


Proof. Let $U$ and $V$ be two states in $A'$ that cannot be distinguished. This means that for any string $w^R$ we have $\delta'(U,w^R) \in F'$ iff $\delta'(V,w^R) \in F'$. We show that now $U$ and $V$ are equal.

By the construction of $F'$ we can rephrase indistinguishability as $\delta'(U,w^R) \ni q_0$ iff $\delta'(V,w^R) \ni q_0$. 

Apply the Basic Observation, and we have $\delta(q_0,w) \in U$ iff $\delta(q_0,w) \in V$.

From this equality $U=V$ follows, as all states in $Q$ are assumed to be reachable, thus for any state $p$ in $U$ or $V$ there is a string $w$ such that $p = \delta(q_0,w)$.
end-of-proof.

But even after proving, the result is still real magic!