Chapter 20 - van Emde Boas Trees

Chapter 20 starts with a first-pass van Emde Boas universe decomposition and a finite-set specification model. The current Lean surface proves high/low/index arithmetic, including bounded high/low recomposition facts, and the correctness of membership, extrema, successor, predecessor, insert, and delete against a represented finite set, including empty-result specifications for extrema, successor, and predecessor plus membership-, extrema-, and neighbor-query-after-update positive and no-neighbor specifications, successful-query universe-bound corollaries, direct no-neighbor query wrappers, premise-light no-neighbor wrappers over old represented sets, direct base extrema/neighbor nonempty-result wrappers, direct updated-neighbor nonempty-result wrappers, direct deletion-extrema nonempty-result wrappers, direct extrema membership/lower- and upper-bound wrappers, direct base/insert/delete neighbor membership/order wrappers, direct extrema-after-update membership/order wrappers, extrema empty-after-update specifications, direct extrema empty-result wrappers, update-query universe-bound corollaries, direct inserted/deleted key and old-key member-preservation corollaries, exact failed member-query specifications after updates, direct failed member-query preservation wrappers, and operation-depth base/step/linear and monotonicity wrappers.

Sections

• 20.1 Universe decomposition: proved for the first-pass side-length arithmetic. Main results: CLRS.Chapter20.VEB.index_high_low, CLRS.Chapter20.VEB.high_index, CLRS.Chapter20.VEB.low_index, CLRS.Chapter20.VEB.index_lt, CLRS.Chapter20.VEB.high_lt, and CLRS.Chapter20.VEB.low_lt.

• 20.2 Tree specification: partial. Main results: CLRS.Chapter20.VEB.member_correct, CLRS.Chapter20.VEB.member_lt_univ, CLRS.Chapter20.VEB.minimum_correct, CLRS.Chapter20.VEB.minimum_mem, CLRS.Chapter20.VEB.minimum_le, CLRS.Chapter20.VEB.minimum_lt_univ, CLRS.Chapter20.VEB.minimum_none_iff, CLRS.Chapter20.VEB.minimum_none_of_empty, CLRS.Chapter20.VEB.minimum_ne_none_of_nonempty, CLRS.Chapter20.VEB.maximum_correct, CLRS.Chapter20.VEB.maximum_mem, CLRS.Chapter20.VEB.le_maximum, CLRS.Chapter20.VEB.maximum_lt_univ, CLRS.Chapter20.VEB.maximum_none_iff, CLRS.Chapter20.VEB.maximum_none_of_empty, CLRS.Chapter20.VEB.maximum_ne_none_of_nonempty, CLRS.Chapter20.VEB.successor_correct, CLRS.Chapter20.VEB.successor_mem, CLRS.Chapter20.VEB.successor_gt, CLRS.Chapter20.VEB.successor_le, CLRS.Chapter20.VEB.successor_lt_univ, CLRS.Chapter20.VEB.successor_none_iff, CLRS.Chapter20.VEB.successor_none_of_no_gt, CLRS.Chapter20.VEB.successor_ne_none_of_exists_gt, CLRS.Chapter20.VEB.predecessor_correct, CLRS.Chapter20.VEB.predecessor_mem, CLRS.Chapter20.VEB.predecessor_lt, CLRS.Chapter20.VEB.le_predecessor, CLRS.Chapter20.VEB.predecessor_lt_univ, CLRS.Chapter20.VEB.predecessor_none_iff, CLRS.Chapter20.VEB.predecessor_none_of_no_lt, CLRS.Chapter20.VEB.predecessor_ne_none_of_exists_lt, CLRS.Chapter20.VEB.insert_correct, CLRS.Chapter20.VEB.insert_member_iff, CLRS.Chapter20.VEB.insert_member_lt_univ, CLRS.Chapter20.VEB.insert_member_self, CLRS.Chapter20.VEB.insert_member_old, CLRS.Chapter20.VEB.insert_member_false_iff, CLRS.Chapter20.VEB.insert_member_false_of_ne, CLRS.Chapter20.VEB.insert_minimum_correct, CLRS.Chapter20.VEB.insert_minimum_mem, CLRS.Chapter20.VEB.insert_minimum_mem_old_of_ne, CLRS.Chapter20.VEB.insert_minimum_le_inserted, CLRS.Chapter20.VEB.insert_minimum_le_old, CLRS.Chapter20.VEB.insert_minimum_lt_univ, CLRS.Chapter20.VEB.insert_minimum_none_iff, CLRS.Chapter20.VEB.insert_minimum_ne_none, CLRS.Chapter20.VEB.insert_maximum_correct, CLRS.Chapter20.VEB.insert_maximum_mem, CLRS.Chapter20.VEB.insert_maximum_mem_old_of_ne, CLRS.Chapter20.VEB.insert_maximum_inserted_le, CLRS.Chapter20.VEB.insert_maximum_old_le, CLRS.Chapter20.VEB.insert_maximum_lt_univ, CLRS.Chapter20.VEB.insert_maximum_none_iff, CLRS.Chapter20.VEB.insert_maximum_ne_none, CLRS.Chapter20.VEB.insert_successor_correct, CLRS.Chapter20.VEB.insert_successor_mem, CLRS.Chapter20.VEB.insert_successor_mem_old_of_ne, CLRS.Chapter20.VEB.insert_successor_gt, CLRS.Chapter20.VEB.insert_successor_le, CLRS.Chapter20.VEB.insert_successor_lt_univ, CLRS.Chapter20.VEB.insert_successor_none_iff, CLRS.Chapter20.VEB.insert_successor_none_of_no_gt, CLRS.Chapter20.VEB.insert_successor_none_of_insert_le_old_no_gt, CLRS.Chapter20.VEB.insert_successor_ne_none_of_insert_gt, CLRS.Chapter20.VEB.insert_successor_ne_none_of_old_gt, CLRS.Chapter20.VEB.insert_predecessor_correct, CLRS.Chapter20.VEB.insert_predecessor_mem, CLRS.Chapter20.VEB.insert_predecessor_mem_old_of_ne, CLRS.Chapter20.VEB.insert_predecessor_lt, CLRS.Chapter20.VEB.insert_le_predecessor, CLRS.Chapter20.VEB.insert_predecessor_lt_univ, CLRS.Chapter20.VEB.insert_predecessor_none_iff, CLRS.Chapter20.VEB.insert_predecessor_none_of_no_lt, CLRS.Chapter20.VEB.insert_predecessor_none_of_query_le_insert_old_no_lt, CLRS.Chapter20.VEB.insert_predecessor_ne_none_of_insert_lt, CLRS.Chapter20.VEB.insert_predecessor_ne_none_of_old_lt, CLRS.Chapter20.VEB.delete_correct, CLRS.Chapter20.VEB.delete_member_iff, CLRS.Chapter20.VEB.delete_member_lt_univ, CLRS.Chapter20.VEB.delete_member_deleted_false, CLRS.Chapter20.VEB.delete_member_of_ne, CLRS.Chapter20.VEB.delete_member_false_iff, CLRS.Chapter20.VEB.delete_member_false_old, CLRS.Chapter20.VEB.delete_member_false_of_eq, CLRS.Chapter20.VEB.delete_minimum_correct, CLRS.Chapter20.VEB.delete_minimum_ne, CLRS.Chapter20.VEB.delete_minimum_mem, CLRS.Chapter20.VEB.delete_minimum_le_old, CLRS.Chapter20.VEB.delete_minimum_lt_univ, CLRS.Chapter20.VEB.delete_minimum_none_iff, CLRS.Chapter20.VEB.delete_minimum_none_of_all_eq, CLRS.Chapter20.VEB.delete_minimum_ne_none_of_remaining, CLRS.Chapter20.VEB.delete_maximum_correct, CLRS.Chapter20.VEB.delete_maximum_ne, CLRS.Chapter20.VEB.delete_maximum_mem, CLRS.Chapter20.VEB.delete_maximum_old_le, CLRS.Chapter20.VEB.delete_maximum_lt_univ, CLRS.Chapter20.VEB.delete_maximum_none_iff, CLRS.Chapter20.VEB.delete_maximum_none_of_all_eq, CLRS.Chapter20.VEB.delete_maximum_ne_none_of_remaining, CLRS.Chapter20.VEB.delete_successor_correct, CLRS.Chapter20.VEB.delete_successor_mem, CLRS.Chapter20.VEB.delete_successor_gt, CLRS.Chapter20.VEB.delete_successor_le, CLRS.Chapter20.VEB.delete_successor_lt_univ, CLRS.Chapter20.VEB.delete_successor_none_iff, CLRS.Chapter20.VEB.delete_successor_none_of_no_gt, CLRS.Chapter20.VEB.delete_successor_none_of_old_no_gt, CLRS.Chapter20.VEB.delete_successor_ne_none_of_remaining_gt, CLRS.Chapter20.VEB.delete_predecessor_correct, CLRS.Chapter20.VEB.delete_predecessor_mem, CLRS.Chapter20.VEB.delete_predecessor_lt, CLRS.Chapter20.VEB.delete_le_predecessor, CLRS.Chapter20.VEB.delete_predecessor_lt_univ, CLRS.Chapter20.VEB.delete_predecessor_none_iff, CLRS.Chapter20.VEB.delete_predecessor_none_of_no_lt, CLRS.Chapter20.VEB.delete_predecessor_none_of_old_no_lt, CLRS.Chapter20.VEB.delete_predecessor_ne_none_of_remaining_lt, CLRS.Chapter20.VEB.operationDepth_zero, CLRS.Chapter20.VEB.operationDepth_succ, CLRS.Chapter20.VEB.operationDepth_linear, CLRS.Chapter20.VEB.operationDepth_monotone, and CLRS.Chapter20.VEB.operationDepth_strict_mono.

Current Gaps

Recursive summary/cluster storage, word-RAM base cases, and a Chapter 3 asymptotic bridge for O(log log u) remain strengthening targets.