English
Given valid left and right partitions and a size-balance hypothesis, the balanced right-branch construction is valid.
Русский
Имея допустимые левые и правые разбиения и гипотезу баланса размеров, корректна правая ветка балансировки.
LaTeX
$$$\\forall l x r o_1 o_2,\\; \\mathrm{Valid'} o_1 l (\\mathrm{WithTop}.some x) \\to \\mathrm{Valid'} (WithBot.some x) r o_2 \\to \\cdots \\Rightarrow \\mathrm{Valid'} o_1 (l.balanceR x r) o_2$$$
Lean4
theorem balanceR_aux {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H₁ : size r = 0 → size l ≤ 1)
(H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r) (H₃ : 2 * @size α r ≤ 9 * size l + 5 ∨ size r ≤ 3) :
Valid' o₁ (@balanceR α l x r) o₂ := by
rw [Valid'.dual_iff, dual_balanceR]
have := hr.dual.balanceL_aux hl.dual
rw [size_dual, size_dual] at this
exact this H₁ H₂ H₃
