English
Let l and r be balanced binary trees with root x, and suppose their sizes are sl and sr respectively. If the balancing condition H holds (involving possible raises and balanced sizes), then a predicate P holds for all nodes of balanceL(l, x, r) if and only if P holds for all nodes of l, P holds for x, and P holds for all nodes of r.
Русский
Пусть l и r — сбалансированные двоичные дерева с корнем x, размеры которых равны sl и sr. При выполнении условия балансировки H (с учетом возможного подъема и сбалансированных размеров) утверждение: для любого предиката P верно, что P выполняется для всех узлов balanceL(l, x, r) тогда и только тогда, когда P выполняется для всех узлов l, P выполняется для x и P выполняется для всех узлов r.
LaTeX
$$$\forall P\ l\ x\ r,\ l\ Balanced\ ∧\ r\ Balanced\ ∧\ sl\ Sized\ l\ ∧\ sr\ Sized\ r\ ∧\ H,\ All\ P\ (balanceL\ l\ x\ r) \iff (All\ P\ l) \land P\ x \land (All\ P\ r)$$$
Lean4
theorem all_balanceL {P l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
(H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') :
All P (@balanceL α l x r) ↔ All P l ∧ P x ∧ All P r := by rw [balanceL_eq_balance' hl hr sl sr H, all_balance']
