English
Internal splitMin' returns the minimum element xm from the left spine and the remaining tree l' after removing xm from the tree, balancing on the way up.
Русский
Внутреннее разбиение splitMin' возвращает минимальный элемент xm слева и оставшееся дерево l' после удаления xm, со слиянием по мере подъема.
LaTeX
$$$$ \mathrm{splitMin'}: \ Ordnode\; \alpha \to \alpha \to \ Ordnode\; \alpha \to \ alpha \times \ Ordnode\; \alpha, \\ (\text{nil}, x, r) \mapsto (x, r), \\ (\mathrm{node}\; - \; ll \; lx \; lr) \mapsto \big( xm, \mathrm{balanceR}(l', x, r) \big) $$ where $ (xm, l') = \mathrm{splitMin'}(ll, lx, lr) $$$
Lean4
/-- **Internal use only**, because it requires a balancing constraint on the inputs.
O(log n). Extract and remove the minimum element from a nonempty tree. -/
def splitMin' : Ordnode α → α → Ordnode α → α × Ordnode α
| nil, x, r => (x, r)
| node _ ll lx lr, x, r =>
let (xm, l') := splitMin' ll lx lr
(xm, balanceR l' x r)
