bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def certificate
law leaf_comparison
law leaf_lookup
law lift_left
law lift_right
law branch
law lookup_certificate
law returned_value_is_storedNo tree validity premise is needed for this direction.
def listedIndependent list membership for actual Map.to_list output.
law accumulator_included
law leaf_enumerated
law returned_value_enumerated

def truthLogical forms of the existing executable routing predicates.
law false_true
law and_left
law and_right
law equal_bit
def routed
law route_projection
law routed_certificate
def validThis weaker property is precisely the part of critbit needed for lookup.
law member_routed
def copies_left
def copies_right
law duplicate_memberStructural duplication of a membership witness; no unrestricted Type cast.
law lookup_leftConverse of native lookup soundness.
law lookup_right
law member_lookup
law critbit_certificate
law critbit_member_lookup

def strideThe binary constructor in the independent specification uses Base Nat.divmod.
def binary_division
def binary_quotient
def binary_remainder
def bit_roundtrip
def binary_constructor
def regroupReconstruct the low n bits after adding ANY multiple of 2^n.
def reconstruct
def add_refines_nActual full-width ripple addition equals independent mathematical conversion.
def add_refines
def time_add_refines
def increment_refinesThe same reconstruction discharges wraparound for every metric counter.
def counter_refines

def subtract_sumArithmetic cancellation against actual Base Nat.sub, with no bounds premise.
def complementary_digits
def complement_sumComplement and original together, plus one, are exactly 2^width.
def complement_distance
def negation_refinesActual two's-complement negation refines mathematical modular subtraction at every width, including zero and the signed minimum pattern.
def native_negation_refinesThis concrete theorem reaches the actual fixed-width implementation without normalizing a 2^64 unary Nat literal in the checker.

def succ_equalCommutative-semiring laws of Base Nat.add/Nat.mul, by induction on the actual definitions.
def add_zero
def add_succ
def add_comm
def add_assoc
def add_swapa + (b + c) == b + (a + c)
def mul_zero
def mul_succ
def mul_comm
def mul_one
def mul_add_right
def mul_add_left
def mul_assoc
def double_add
def double_self
def double_mul