English
If left subtree l and middle subtree m and right subtree r form a balanced chain with specified balanced sizes, then the three-way node is valid on the right formation.
Русский
Если левые, средние и правые поддеревья образуют сбалансированную цепочку размеров, то узел node3R допустим в правой конфигурации.
LaTeX
$$$\\forall {l} {x} {m} {y} {r} {o_1} {o_2},\\; (hl: Valid'(o_1, l, x)) \\wedge (hm: Valid'(x, m, y)) \\wedge (hr: Valid'(y, r, o_2)) \\wedge (H1: BalancedSz(size(l), size(m) + size(r) + 1)) \\wedge (H2: BalancedSz(size(m), size(r))) \\Rightarrow Valid'(o_1, (l.node3R x m y r), o_2).$$$
Lean4
theorem node3R {l} {x : α} {m} {y : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hm : Valid' x m y) (hr : Valid' y r o₂)
(H1 : BalancedSz (size l) (size m + size r + 1)) (H2 : BalancedSz (size m) (size r)) :
Valid' o₁ (@node3R α l x m y r) o₂ :=
hl.node' (hm.node' hr H2) H1
