# Red black tree - Insert/Delete proof of correctness

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.

• Understanding how red-black trees work is definitely not best approached looking at the code. Have a look at the pictures and diagrams in the book. They precisely show the heights of respective subtrees before and after rotation at a certain node. Insertion is probably not proved by induction, as there is just a precise node where the rotation occurs. – Hendrik Jan Apr 25 '16 at 9:08
• I actually looked at the pictures, however shouldn't I use the pseudo-code to prove it? – user8469759 Apr 25 '16 at 9:10
• From the code I do not see what is happening. From the pictures I can construct the code. – Hendrik Jan Apr 25 '16 at 12:32
• So what approach do you suggest? I don't actually understand what are you trying to suggest. – user8469759 Apr 25 '16 at 13:16
• So, any thoughts about my question? – user8469759 May 6 '16 at 8:16