Persistent binary search tree deletion
= Persistent binary search tree deletion
A <pure function> deletes a key from a <binary search tree> by rebuilding its search path and sharing untouched subtrees. At a matching node with two children, replace its key by the least key in its right subtree, removing that occurrence from the right subtree. The ordering invariant is preserved, with <time complexity> and fresh-node allocation proportional to the <height of a binary tree>.