English
Internal splitMax' returns the tree with the maximum element removed and its value xm, traversing from the right and balancing on the way up.
Русский
Внутреннее разбиение splitMax' возвращает дерево без максимального элемента и значение xm, обходя дерево справа и балансируя по мере подъема.
LaTeX
$$$$ \mathrm{splitMax'}: \ Ordnode\; \alpha \to \alpha \to \ Ordnode\; \alpha \to \ Ordnode\; \alpha \times \alpha, \\ (l, x, nil) = (l, x), \\ (l, x, node\; _\; rl \; rx \; rr) = \big( \mathrm{balanceL}(l, x, r'), xm \big) $$ where $ (r', xm) = \mathrm{splitMax'}(rl, rx, rr) $$$
Lean4
/-- **Internal use only**, because it requires a balancing constraint on the inputs.
O(log n). Extract and remove the maximum element from a nonempty tree. -/
def splitMax' : Ordnode α → α → Ordnode α → Ordnode α × α
| l, x, nil => (l, x)
| l, x, node _ rl rx rr =>
let (r', xm) := splitMax' rl rx rr
(balanceL l x r', xm)
