English
Let l, x, m, y, r be subtrees/nodes with m sized. Then the size of the node4L constructed from these parts equals the sum of the sizes of l, m, r plus 2: size(node4L(l, x, m, y, r)) = size(l) + size(m) + size(r) + 2.
Русский
Пусть l, m, r — поддеревья, m упорядочено по размеру. Тогда размер узла node4L(l, x, m, y, r) равен сумме размеров вложенных поддеревьев плюс 2: size(node4L(l, x, m, y, r)) = size(l) + size(m) + size(r) + 2.
LaTeX
$$$\operatorname{size}(\mathrm{node4L}(l, x, m, y, r)) = \operatorname{size}(l) + \operatorname{size}(m) + \operatorname{size}(r) + 2$$$
Lean4
theorem node4L_size {l x m y r} (hm : Sized m) : size (@node4L α l x m y r) = size l + size m + size r + 2 :=
by
cases m
· simp [node4L, node3L, node']
abel
· simp [node4L, node', size, hm.1]; abel
