bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def sc
def mul_sc
def mul_sc1
def sc_mul
def sc_le
def sc_lt
def sc_lt_cancel_g
def sc_lt_cancel
def le_sc
def digit_lta digit x below 2^k after y < b scaled by 2^k stays below b scaled
def mul_le
def one_mul
def quot_lt_g
def quot_ltq d + r < 2^k d forces q < 2^k
def stepone long-division step: if x == q d + r and 2^k r + y == q2 d + r2 then 2^k x + y == (2^k q + q2) d + r2
def go_le
def div_lea quotient never exceeds its dividend
def zsub
def sub_cancel_l
def sc_idx2^(k + j) x == 2^k (2^j x)
def sc_sub2^k (a - b) == 2^k a - 2^k b
def sub_le2a - b <= a

def sum_bitCarry is computed from input bits; it is not an assumed property of Word.add.
def carry_bit
def carry_out
law bit_conservation
law lift_conservation
law adc_shape
law step
law adc_conservation
law addition_conservationA full-width arithmetic law linked to the actual cache deadline adder.

def carryCarry out is mathematical all-bits-set, not an assumed increment result.
law scale_zero
law increment_conservationExact integer conservation for the installed ripple increment at every width: result + (carry-out * 2^width) = input + 1.
law counter_conservation

def candidateA long-division candidate is less than twice the divisor for either input bit.
def cancel_less
def ge_reverse
def not_ge
def subtract_boundSubtracting the divisor once restores the strict remainder bound.

def times_two
def doublingThe actual U32 multiplication in wide.digit computes low bits of 2*r.
def shift_value
def multiplication_is_shift
def digitLink directly to the recurrence used by actual div_million.

def remainder
def not_ge
def resultBoth branches refer to actual wide.digit_result, not a proof-side divider.
def compare
def digit
def boundedEvery recursively reached remainder of the executed divider is strictly below the divisor, for arbitrary widths and inputs.

def higher_leHigher-bit comparison cannot be greater if the complete comparison is <=.
def high_monotone
def discarded
def bits
def bounded_carryThe concrete divisor is handled as a native 32-bit word, avoiding expansion of a million unary constructors.
def exact_without_carry
def decoded_candidate
def candidate_value
def decoded_high
def double_value
def high_candidate

def below_successor
def identify
def quotient
def recognizes
def natural_quotient
def reconstruct
def word_quotient
def specification_equation
def guarded
def actual
def native_projection
def unsigned_millisecondsConnection to the actual duration core and the public independent numeric specification's nonnegative branch.

def subtractGeneral U32 subtraction branch; comparison and decoded subtraction are both justified by the actual Base definitions, and the input range is explicit.
def subtract_native
def millionConcrete executed subtraction restores the native remainder bound.
def subtraction_conservation

def add_zeroAdding the incoming bit to an even shifted word changes only its low bit.
def bit_word
def add_bit
def primitive_bit
def shifted
def actual_candidateThis is the exact candidate expression executed in wide.digit.
def exactThe range premise concerns the inputs and discharges discarded carry.

def valueA mathematical observation of the actual returned quotient and remainder.
def selected
def selection_value
def result_formNormal form of the actual helper; the denominator identity is explicit.
def weight_step
def result_value
def gather
def digit