From the Cormen book I was studying the chapter focused on the red black tree. I was particularly interested in why the procedures for insert/delete fixup works (namely a formal proof).
I report both the algorithms, taken from the book:
The book gives a generic explanation of why they works, but doesn't give any formal proof. Could you suggest me how to prove the result, or could where I find the proof? For example if I focus on the insert, I would look at the node $z$ and I would assume by induction that one subtree has black height $h-1$ while the other has black height $h$, then I would show that after an iteration both subtree have black height $h$. I would try something similar for the delete procedure.
I'm not entirely sure that this is the best way to prove the correctness, and I can't actually find a formal proof of the result.
(The main reason is actually that every time I read the book and specifically such chapter I just try to memorize the procedures. Since this kind of tree implementation is quite common I think is time I understand why it works.