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.
Русский
Если левые, средние и правые поддеревья образуют сбалансированную цепочку размеров, то узел node3L допустим.
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))) \\wedge (H2: BalancedSz(size(l) + size(m) + 1, size(r))) \\Rightarrow Valid'(o_1, (l.node3L x m y r), o_2).$$$
Lean4
theorem node3L {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)) (H2 : BalancedSz (size l + size m + 1) (size r)) :
Valid' o₁ (@node3L α l x m y r) o₂ :=
(hl.node' hm H1).node' hr H2
