bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def periodComplete one period of the existing Base countdown division.
def stride
def small
def decompositionEuclidean decomposition is recognized by actual Base Nat.divmod for every positive divisor and arbitrary quotient, from the mathematical remainder bound.
def quotientQuotient and remainder projections used by the independent duration model.
def remainder

def interchangeElementary semiring equations proved over the existing Base Nat definitions.
def shuffle
def distribute
def double_sum
def double_product
def multiply_double
def scale_sum
def scale_product

def carry_complementThe increment after complement overflows precisely for a zero input.
def sign_nonzero
def magnitudeNo overflow premise is assumed: nonzero input determines the actual carry.
def twice
def scale_power

law increment_maximum_wrapsArbitrary-width rollover law, not an enumerated 64-bit test.
law zero_detected
law zero_sign
law divide_zero
law immortal_duration
law immortal_deadline
law counter_rolloverChecked connection between the public wrapping counter operation and the arbitrary-width rollover theorem, independent of capacity or trace length.
law split_join
law pack_roundtrip
def rejoin
law rejoin_cons
law join_split
law comparison_low_zero_geNumeric specification defines sign by comparison with the high-bit threshold; executable code reads the last bit.
law sign_threshold_correspondence
law comparison_low_zero_eq
law zero_comparison_correspondence
law signed_order_branches
law signed_order_refines
law expiration_sentinel_branch
law expiration_refines
law double_add
law primitive_word_interpretation
law join_interpretation
law pack_interpretation

def complementary_differenceIf both minuends contain b, rearrange their complementary differences.
def predecessor
def cancel_left
def solveA bounded machine result and the actual carry conservation determine the subtraction result uniquely; no no-borrow premise is assumed.
def exactExact interpretation of executed Base subtraction when a >= b.
def primitive_bound
def u32_exact

def refinesActual Base ripple addition, at any width, with exact modulo interpretation.
def u32_refinesPrimitive U32 decoding is connected to that same independent interpretation.
def with_carry

law doubled_bound
law unsigned_boundIndependent interpretation of every n-bit word lies in [0, 2^n).

def excessOverflow is calculated from input bits and the existing primitive carries.
def restore_shift
def swap_last
def restore_addition
def conservationInduction follows the actual multiplier's bit loop and restores every carry.