English
The merge of two adjacent nodes is given by a piecewise expression: it is either a balanced-left merge, a balanced-right merge, or a glue of the two nodes, depending on the sizes and delta.
Русский
Слияние двух соседних узлов задаётся по-разному: либо балансировка слева, либо балансировка справа, либо сцепление двух узлов, в зависимости от размеров и параметра delta.
LaTeX
$$merge( node α ls ll lx lr, node rs rl rx rr) = if delta*ls < rs then balanceL (merge (node ls ll lx lr) rl) rx rr else if delta*rs < ls then balanceR ll lx (merge lr (node rs rl rx rr)) else glue (node ls ll lx lr) (node rs rl rx rr)$$
Lean4
@[simp]
theorem merge_node {ls ll lx lr rs rl rx rr} :
merge (@node α ls ll lx lr) (node rs rl rx rr) =
if delta * ls < rs then balanceL (merge (node ls ll lx lr) rl) rx rr
else
if delta * rs < ls then balanceR ll lx (merge lr (node rs rl rx rr))
else glue (node ls ll lx lr) (node rs rl rx rr) :=
rfl
