English
If hl and hr are valid and certain size-constraints hold, balanceL yields a valid result with a balanced partition.
Русский
Если hl и hr валидны и выполняются некоторые ограничения по размерам, balanceL даёт валидный результат с балансированным разбиением.
LaTeX
$$$ \forall l,x,r.\ hl\land hr\land (H_1 \lor H_2)\Rightarrow \mathrm{Valid}'(o_1, \mathrm{balanceL}(l,x,r)) o_2$$$
Lean4
theorem balanceL_aux {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H₁ : size l = 0 → size r ≤ 1)
(H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l) (H₃ : 2 * @size α l ≤ 9 * size r + 5 ∨ size l ≤ 3) :
Valid' o₁ (@balanceL α l x r) o₂ :=
by
rw [balanceL_eq_balance hl.2 hr.2 H₁ H₂, balance_eq_balance' hl.3 hr.3 hl.2 hr.2]
refine hl.balance'_aux hr (Or.inl ?_) H₃
rcases Nat.eq_zero_or_pos (size r) with r0 | r0
· rw [r0]; exact Nat.zero_le _
rcases Nat.eq_zero_or_pos (size l) with l0 | l0
· rw [l0]; exact le_trans (Nat.mul_le_mul_left _ (H₁ l0)) (by decide)
replace H₂ : _ ≤ 3 * _ := H₂ l0 r0; cutsat
