1. CLRS-Lean
  2. CLRS Fourth Edition
  3. Chapter 18. B-Trees
  4. 18.3. B-Tree Deletion
  5. Delete Preserves ChildBounded
Imports
import CLRSLean.FourthEdition.Chapter_18.Section_18_3_B_Tree_Deletion.ComposedPreservation

B-tree deletion: child-bound projection

This submodule retains the public composedDelete_childBounded name as a small projection from the bundled raw-deletion preservation theorem.

namespace CLRSnamespace Chapter18namespace BTree

Raw deletion preserves recursive child key ranges for a structurally well-formed input node.

lemma composedDelete_childBounded (t x : Nat) (ht : 2 ≤ t) (tr : BTree) {isRoot : Bool} (hinv : NodeWF t isRoot tr) : ChildBounded (composedDelete t x tr) := by exact (composedDelete_rootResult t x ht (hinv.asRoot ht)).2.1.2.1
end BTreeend Chapter18end CLRS