English
If l and r are balanced with sizes sl and sr and the usual balancing hypotheses hold, then the size of balanceR(l, x, r) is size(l) + size(r) + 1.
Русский
Если l и r сбалансированы и выполняются обычные условия балансировки, то размер balanceR(l, x, r) равен размеру l плюс размеру r плюс 1.
LaTeX
$$$\forall l\ x\ r,\ hl:\ Balanced\ l\ ∧ hr:\ Balanced\ r\ ∧ sl:\ Sized\ l\ ∧ sr:\ Sized\ r\ ∧ H,\ size(balanceR\ l\ x\ r) = size(l) + size(r) + 1$$$
Lean4
theorem size_balanceR {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
(H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
size (@balanceR α l x r) = size l + size r + 1 := by rw [balanceR_eq_balance' hl hr sl sr H, size_balance' sl sr]
