English
In an ordered binary tree (Ordnode) with balanced left subtree l and right subtree r, if the sizes satisfy the required balance hypotheses and there is a suitable Raised element, then the size of balanceL l x r equals size l + size r + 1.
Русский
В упорядоченном двоичном дереве (Ordnode) с сбалансированными левой и правой поддеревьями l и r, при удовлетворении условий баланса и наличии подходящего элемента Raised, размер balanceL l x r равен size l + size r + 1.
LaTeX
$$$ size (balanceL\\, l\\, x\\, r) = size\\, l + size\\, r + 1 $$$
Lean4
theorem size_balanceL {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') :
size (@balanceL α l x r) = size l + size r + 1 := by rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]
