English
Let α be a type with a preorder; balance' relates two subtrees l and r and their sizes under a detailed matrix of inequalities, ensuring the resulting structure preserves validity.
Русский
Пусть α — множество с предшествованием; balance' связывает два поддерева l и r и их размеры по совокупности неравенств, обеспечивая сохранение валидности строения.
LaTeX
$$$ \forall α\ l\ r.\ balance'\_lemma( l, r ) \Rightarrow \mathrm{Valid}'(l) \land \mathrm{Valid}'(r) \Rightarrow \mathrm{Valid}'(\mathrm{balance}(l,r)) $$$
Lean4
theorem balance' {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
(H :
∃ l' r', BalancedSz l' r' ∧ (Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l')) :
Valid' o₁ (@balance' α l x r) o₂ :=
let ⟨_, _, H1, H2⟩ := H
Valid'.balance'_aux hl hr (Valid'.balance'_lemma H1 H2) (Valid'.balance'_lemma H1.symm H2.symm)
