English
In an ordered tree, rotating left at a node yields a specific resulting node depending on the comparison between the size of the left subtree m and a ratio times the size of the right subtree r.
Русский
В упорядоченном дереве поворот налево на узле приводит к конкретному новому узлу в зависимости от сравнения размера левого поддерева m и отношения ratio к размеру правого поддерева r.
LaTeX
$$$\\text{rotateL} \\ l\\ x\\ (\\text{node } sz\\ m\\ y\\ r) = \\begin{cases} \\text{node3L } l\\ x\\ m\\ y\\ r, & \\text{если } |m| < \\mathrm{ratio} \\cdot |r| \\\\ \\text{node4L } l\\ x\\ m\\ y\\ r, & \\text{иначе} \\end{cases}$$$
Lean4
theorem rotateL_node (l : Ordnode α) (x : α) (sz : ℕ) (m : Ordnode α) (y : α) (r : Ordnode α) :
rotateL l x (node sz m y r) = if size m < ratio * size r then node3L l x m y r else node4L l x m y r :=
rfl
