English
The left rotation of a node with left subtree l, key x, and right subtree (node sz m y r) yields either node3L or node4L depending on whether size m is less than ratio times size r.
Русский
Левый вращение узла с левым поддеревом l, ключом x и правым поддеревом (node sz m y r) приводит к узлу node3L или node4L в зависимости от того, меньше ли размер m, чем ratio умноженное на размер r.
LaTeX
$$$$\operatorname{rotateL}(l, x, \operatorname{node}(sz, m, y, r)) = \begin{cases} \operatorname{node3L}(l, x, m, y, r) & \text{если } |m| < \operatorname{ratio} \cdot |r|, \\ \operatorname{node4L}(l, x, m, y, r) & \text{иначе}. \end{cases}$$$$
Lean4
theorem rotateR_node (sz : ℕ) (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
rotateR (node sz l x m) y r = if size m < ratio * size l then node3R l x m y r else node4R l x m y r :=
rfl
