bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def conservationThe denominator is a symbolic U32 identified with the actual fixed divisor; the proof observes the actual execution and discharges each recursive bound.
def actualPublic native divisor identity is discharged here, with no external premise.

def memberExecutable representation predicates, not assumed correctness or a map oracle.
def unique
def included
def bit_value
def routed
def nonempty
def below
def same_prefixEvery pair of leaves below a node agrees on every bit strictly before its discriminator.
def prefix_against
def common_prefix
def critbit
def identities
def representation
def string_identity
law initial_representation
law skipped_prefix_rejectedA discriminator at 33 routes these children correctly, yet misses their first differing presence bit at zero.
law lookup_preserves_critbitLookup preserves even the strengthened discriminator/prefix predicate.

def next_quotientExisting Base.divmod quotient translation; no replacement division algorithm.
law quotient_translation
law character_stride
law bit_at_next
law native_character_strideThis exact key-preserving result connects bit positions across String prefixes using the native division and bit traversal definitions.
law add_right_successor
law division_no_wrap
law first_character_division
law native_first_character

def valueProjections of actual native results; no alternative lookup algorithm.
def lookup
def route_bit
law route_pair
law route_shape
law low_value
law high_value
law node_left
law node_right
law leaf_same
law splice_same_bit
law splice_same
law deep_same_bit
law insertion_branch_same
law insertion_sameThis actual native insertion law needs no well-formedness assumption: querying the new key follows the same bits used to choose its newly inserted leaf.
def seek_found
law seek_low_found
law seek_high_found
law seek_left
law seek_right
law replace_left
law replace_right
def replacement_certificate
law certificate_left
law certificate_right
law certificate_branch
law replacement_at_seek
law seek_low_shape
law seek_high_shape
law seek_branch_shape
law seek_shape
law set_comparison_case
law set_found_case
law set_seek_case
law set_samePublic native Map update/lookup same-key law.