English
O(log n). Remove the i-th element from the tree, counted from the left, returning the resulting tree.
Русский
O(log n). Удалить i-й элемент дерева, считая слева направо, вернуть полученное дерево.
LaTeX
$$$$ \mathrm{removeNth}: \ Ordnode\; \alpha \to \mathbb{N} \to \ Ordnode\; \alpha, \quad \text{nil} \to \text{nil}, \\ \mathrm{removeNth}(\mathrm node\; l\; x\; r, i) = \begin{cases} \text{balanceR}(\text{removeNth}(l,i), x, r) & \text{if } i < |l| \\ \text{glue}(l,r) & \text{if } i = |l| \\ \text{balanceL}(l,x)(\mathrm{removeNth}(r,i-|l|-1)) & \text{if } i > |l| \end{cases} $$$$
Lean4
/-- O(log n). Remove the `i`th element of the set, by its index from left to right.
remove_nth {a, b, c, d} 2 = {a, b, d}
remove_nth {a, b, c, d} 5 = {a, b, c, d} -/
def removeNth : Ordnode α → ℕ → Ordnode α
| nil, _ => nil
| node _ l x r, i =>
match Nat.psub' i (size l) with
| none => balanceR (removeNth l i) x r
| some 0 => glue l r
| some (j + 1) => balanceL l x (removeNth r j)
