English
The validity predicate for an Ordnode subtree asserts that size fields are correct, the tree is balanced, and the elements are ordered according to the preorder-based order.
Русский
Говорящая о корректности поддерева: поля размера верны, дерево сбалансировано, элементы упорядочены согласно заданному порядку.
LaTeX
$$$$ \mathrm{Valid}: \ Ordnode\; \alpha \to \mathrm{Prop} , \quad \mathrm{Valid}(t) := \mathrm{Valid'}\;\bot\; t\; \top $$$$
Lean4
/-- The validity predicate for an `Ordnode` subtree. This asserts that the `size` fields are
correct, the tree is balanced, and the elements of the tree are organized according to the
ordering. -/
def Valid (t : Ordnode α) : Prop :=
Valid' ⊥ t ⊤
