English
If the components satisfy a joint balance condition, then balance(l,x,r) yields a valid node.
Русский
Если компоненты удовлетворяют совместному условию баланса, то balance(l,x,r) даёт допустный узел.
LaTeX
$$$ \forall l,x,r.\ \mathrm{Valid}'(o_1,l) \land \mathrm{Valid}'(x,r) \Rightarrow \mathrm{Valid}'(o_1, \mathrm{balance}(l,x,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₂ := by rw [balance_eq_balance' hl.3 hr.3 hl.2 hr.2]; exact hl.balance' hr H
