Изменения

Если рассмотреть лист(фиктивную вершину), то для нее лемма верна. Рассмотрим внутреннюю вершину <tex>x</tex>. Пусть <tex>hb(x)=h'</tex>. Тогда если ее потомок <tex>p</tex> {{- --}} черный, то высота <tex>hb(p)=h'-1</tex>, а если – красный, то <tex>hb(p)=h'</tex>. Таким образом, по предположению индукции, в поддеревьях содержится не менее <tex>2^{h'}-1</tex> вершин, а во всём дереве, соответственно, не менее <tex>2^{h'}-1 + 2^{h'}-1 + 1=2^{h'+1}-1</tex>.

Каждый элемент вставляется вместо листа, поэтому для выбора места вставки идём от корня до тех пор, пока указатель на следующего сына не станет <tex>nil</tex>(то есть этот сын {{- --}} лист). Вставляем вместо него новый элемент с <tex>nil</tex>-потомками и красным цветом. Теперь проверяем балансировку. Если отец нового элемента красный, то достаточно рассмотреть только два случая:

1. "Дядя" этого узла тоже красный. Тогда просто перекрашиваем "отца" и "дядю" в чёрный цвет, а "деда" {{- --}} в красный. Проверяем, не нарушает ли он теперь балансировку. Если в результате этих перекрашиваний мы дойдём до корня, то в нём в любом случае ставим чёрный цвет.