我不太明白为什么CLRS提供的从二叉搜索树中删除节点的算法（见下文）能够正常工作（比如我们如何知道节点的有序排列将以正确的方式保持？）；是否有任何正式的证明可以更深入地解释这一点？如果有人能帮助我，我将不胜感激。算法如下：
删除
从二叉搜索树T中删除节点z 的总体策略有三种基本情况，但正如我们将看到的，其中一种情况有点棘手。
- 如果z没有子节点，那么我们只需通过修改其父节点来将其删除，用 NIL 替换z作为其子节点。
- 如果z只有一个孩子，那么我们通过修改z的父节点以用z的孩子节点替换z来提升该孩子节点以取代z在树中的位置。
- 如果z有两个子节点，那么我们找到z的后继节点 y（它必须位于z的右子树中），并让y占据树中z的位置。z的原始右子树的其余部分将成为y的新右子树，z的左子树将成为y的新左子树。这种情况比较棘手，因为正如我们将看到的， y是否是z的右子节点很重要。
我试图通过逐案分析来证明这一点，但这似乎很难。
BST 由以下属性定义：对于每个节点 N，N 左子树中的所有节点都小于 N，并且 N 右子树中的所有节点都大于 N。请注意，这不允许树中存在任何重复项。
在算法的第 1 种情况下，每个节点的子树要么不变，要么丢失一个节点，因此属性保持不变。
案例2也是同样的情况。
在情况 3 中，我们需要证明该属性适用于新形成的树，其根为
y，子树为 。该过程有两个步骤：(a) 移除y和 (b) 用 替换x。y步骤 (a) 的工作方式与上面的情况 1 或 2 相同，因此该属性仍然成立（注意不能有左子节点）。步骤 (b) 也不违反该属性，因为和y之间没有节点。该案例的棘手之处并未影响到证明。xy