English
Given two valid trees with a balanced size condition, glue yields a valid tree and its size equals the sum of the sizes.
Русский
При двух валидных деревьях и условии баланса размеров объединение дает валидное дерево и размер равен их сумме.
LaTeX
$$$\\forall \\text{hl hr bal sep},\\; \\mathrm{Valid'} o_1 (l.glue r) o_2 \\land \\mathrm{size}(glue l r) = \\mathrm{size}(l) + \\mathrm{size}(r)$$$
Lean4
theorem glue {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) :
BalancedSz (size l) (size r) → Valid' o₁ (@glue α l r) o₂ ∧ size (@glue α l r) = size l + size r :=
Valid'.glue_aux (hl.trans_right hr.1) (hr.trans_left hl.1) (hl.1.to_sep hr.1)
