English
If left and right subtrees are valid and the sizes are balanced, then the node is valid.
Русский
Если левые и правые поддеревья допустимы и размеры сбалансированы, то узел допустим.
LaTeX
$$$\\forall s,l,x,r,o_1,o_2:\\; (\\operatorname{Ordnode.Valid}'(o_1,l,x)) \\wedge (\\operatorname{Ordnode.Valid}'(x,r,o_2)) \\wedge (\\operatorname{BalancedSz}(l.\\text{size}, r.\\text{size})) \\Rightarrow \\operatorname{Ordnode.Valid}'(o_1, (\\mathrm{node}\\, s\\, l\\, x\\, r), o_2).$$$
Lean4
theorem node {s l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H : BalancedSz (size l) (size r))
(hs : s = size l + size r + 1) : Valid' o₁ (@node α s l x r) o₂ :=
⟨⟨hl.1, hr.1⟩, ⟨hs, hl.2, hr.2⟩, ⟨H, hl.3, hr.3⟩⟩
