English
Given valid subtrees on both sides and appropriate size-distribution conditions, the auxiliary balancing step preserves validity or yields a balanced split.
Русский
При наличии валидных поддеревьев слева и справа и подходящих условий распределения размеров, вспомогательный шаг балансировки сохраняет валидность или даёт сбалансированное разбиение.
LaTeX
$$$ \forall l, x, r, o_1, o_2,\ hl,\ hr,\ H_1,\ H_2.\ Balance'\_aux(hl, hr, H_1, H_2) : \mathrm{Valid}'(o_1, \mathrm{balance}'(l, x, r))\, o_2 $$$
Lean4
theorem balance'_aux {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
(H₁ : 2 * @size α r ≤ 9 * size l + 5 ∨ size r ≤ 3) (H₂ : 2 * @size α l ≤ 9 * size r + 5 ∨ size l ≤ 3) :
Valid' o₁ (@balance' α l x r) o₂ := by
rw [balance']; split_ifs with h h_1 h_2
· exact hl.node' hr (Or.inl h)
· exact hl.rotateL hr h h_1 H₁
· exact hl.rotateR hr h h_2 H₂
· exact hl.node' hr (Or.inr ⟨not_lt.1 h_2, not_lt.1 h_1⟩)
