English
Under the hypotheses that left and right subtrees are Balanced and Sized, and given a suitable growth condition H, balanceL equals balance'.
Русский
При предположениях, что левые и правые поддеревья сбалансированы и имеют размеры, и дано условие роста H, balanceL = balance'.
LaTeX
$$l.Balanced → r.Balanced → l.Sized → r.Sized → (∃ l', Raised l'(size l) ∧ BalancedSz l' (size r)) ∨ (∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') → @balanceL α l x r = balance' l x r$$
Lean4
theorem balanceL_eq_balance {l x r} (sl : Sized l) (sr : Sized r) (H1 : size l = 0 → size r ≤ 1)
(H2 : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l) : @balanceL α l x r = balance l x r :=
by
obtain - | ⟨rs, rl, rx, rr⟩ := r
· rfl
· obtain - | ⟨ls, ll, lx, lr⟩ := l
· have : size rl = 0 ∧ size rr = 0 := by
have := H1 rfl
rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
cases sr.2.1.size_eq_zero.1 this.1
cases sr.2.2.size_eq_zero.1 this.2
rw [sr.eq_node']; rfl
· replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
simp [balanceL, balance, H2]; split_ifs <;> simp [add_comm]
