bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def carry
def conservationInteger conservation for actual Base.shl.put, retaining the discarded bit.
def same_as_put
def shift_conservation
def refines
def exact

def shape
def flipThe subtraction branch of existing Base.adc equals addition of complemented bits with the same input carry.
def complement_form
def refinesExact modulo subtraction expressed using nonnegative mathematical magnitudes.
def u32_refinesConcrete primitive used in wide.digit_result; the independent complement conservation above gives the equivalent nonnegative modular-subtraction form.

def le_reflEvery natural below 2^n is represented exactly by from_nat(n, v): its unsigned value is v.
def le_succ
def le_add
def shift_count(M + r) + (1 + n) == (M + (1 + r)) + n
def shift_carry(M + r) + (1 + n) == ((1+bp) + M + 0) + n when r == bp
def go_equation
def bound_zero
def extend
def goInvariant of the actual division loop: remaining countdown m plus the running remainder r is the divisor minus one.
def halfv == 2*(v/2) + v%2 and v%2 <= 1, for the actual Nat.divmod.
def remainder_bit
def not_below_zero
def lt_double
def two_times
def rescalev < 2 * 2^p, rewritten as 2*(v/2) + v%2 < double(2^p)
def from_nat_step
def below_one
def half_parts
def from_nat_value