Balance factor changes after local rotations in AVL tree I try to understand balance factors change after local rotations in AVL trees.
Given the rotate_left operation:

  x            y'
 / \          / \
a   y   =&gt;   x'  c
   / \      / \
  b   c    a   b


and $b(x)$, $b(y)$ - balance factors for $x$ and $y$ nodes - I want to find $b(x')$ and $b(y')$.

In my reasoning I will use the Iverson bracket notation, that denotes a number that is 1 if the condition in square brackets is satisfied, and 0 otherwise:
$$
[P]=\begin{cases} 1, \text{ if } P \text{ is true}; \\
              0, \text{ otherwise}.\end{cases} $$

Balance factor for the node $x'$ can be calculated like this:
$$b(x') = h(b) - h(a)$$

where $h(b)$ and $h(a)$ - the heights of sub-trees $a$ and $b$.

Let's substitute $h(b) = h(y) - b(y)[b(y) &gt; 0] - 1$ and $h(a) = h(x) - b(x)[b(x) &gt; 0] - 1$:

$$b(x') = (h(y) - b(y)[b(y) &gt; 0] - 1) - (h(x) - b(x)[b(x) &gt; 0] - 1)$$

Some simplification:

$$b(x') = h(y) - b(y)[b(y) &gt; 0] - h(x) + b(x)[b(x) &gt; 0]$$

Now substitute $h(y) = h(x) + b(x)[b(x) \le 0] - 1 $:

$$b(x') = h(x) + b(x)[b(x) \le 0] - 1 - b(y)[b(y) &gt; 0] - h(x) + b(x)[b(x) &gt; 0]$$

Obviously, $[b(x) \le 0] + [b(x) &gt; 0] = 1$:

$$b(x') = h(x) + b(x) - 1 - b(y)[b(y) &gt; 0] - h(x)$$

Simplify again:

$$b(x') = b(x) - b(y)[b(y) &gt; 0] - 1$$

In the same way I can find balance factor for $y'$. Skipping intermediate steps I get:
$$ b(y') = h(c) - h(x') =\\
     ...\\
     = b(x) + b(y)[b(y) \le 0] - b(x')[b(x') &gt; 0] - 2$$

Somehow I have feeling that this is not the simplest formula for balance factors. 

Is there any simpler approach to calculate balance factors, which would always work even if the tree becomes unbalanced?

EDIT:

The simplest formulas I managed to get look like this (see my own answer for details):
$$b(y′)=b(y)+b(x')[b(x')\le0]−1$$
$$b(x′)=b(x)−b(y)[b(y)&gt;0]−1$$
I found the answer myself.
We know that
$$b(x)=b(x')+b(y)[b(y)&gt;0]+1$$
$$b(y′)=b(x)+b(y)[b(y)\le0]−b(x′)[b(x′)&gt;0]−2$$
thus
$$b(y′)=b(x')+b(y)[b(y)&gt;0]+1+b(y)[b(y)\le0]−b(x′)[b(x′)&gt;0]−2$$
where
$$b(x')−b(x′)[b(x′)&gt;0]=b(x')[b(x')\le0].$$
So, the new balance factors will look like this:
$$b(y′)=b(y)+b(x')[b(x')\le0]−1$$
$$b(x′)=b(x)−b(y)[b(y)&gt;0]−1$$