bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def hlfThe Nat halving the checker can compute structurally (no Nat.div).
def hlf_double
def hlf_double_succ
def hlf_bit
def shr_value
def hlf_le
def hlf_succ_le
def hlf_lowerThe midpoint of a nonempty range lies inside it: a <= hlf(a+b) < b whenever a < b.
def hlf_upper
def hlf_bound
def shr_bridge
def hlf_lts < 2m gives s/2 < m: one narrowing step of a search range that started below 2^f lands below 2^(f-1).
def step_boundThe size after one step is at most s/2, so it stays below the halved bound.
def sub_leU32.sub is exact whenever the subtrahend is not larger (no borrow), so it is the Nat subtraction of the two indices.
def sub_bridge

def sc
def uw
def boa bit worth `one`
def bo_bit
def lt1
def lt1r
def wbevery n-bit word is below 2^n
def uniqr1 + 2^n x == r2 + 2^n y with both r below 2^n forces r1 == r2
def add_exactaddition below 2^n is exact
def mul_exactmultiplication below 2^n is exact
def sub_wrapIf x + 2^n == d + b with d < 2^n, the machine difference x - b is d.
def ob
def ow
def shl_con
def shl_nil
def shl_outthe out-shifted bit and word together hold c + 2w
def shl_out1the same with the out-shifted bit worth `one`
def add_inner
def add_alglow limbs l with carry c0, high limbs t = ah + bh (carry c1), then h = t + c0 (carry c2): the two-limb sum loses exactly 2^(2n) (c1 + c2).
def carry_ltthe carry out of an addition is the wrap-around test sum < x
def not_join
def onesevery bit set
def incif
def inc_joinincrementing a joined word carries into the high part iff the low part is all ones
def eq_fin_tf
def eq_fin_ff
def inc_zeroan increment is zero iff it wrapped from all ones
def one_word
def add_oneadding one is incrementing
def maskthe low k bits set
def hi_partthe bits of x above the low k
def and_false_bv
def and_zero
def low0
def mask_splitx == (x & mask k) + 2^k (bits above k)
def sc_pos
def mask_ltx & mask k is below 2^k
def pw2^k as an n-bit word
def pw_val
def pwva word known to be 2^k has value 2^k (the word stays a variable)
def inc_exactan increment below 2^n is exact

def bit_and_le
def add_le
def and_lemasking never exceeds the mask
def and_le32
def bucket_leTHEOREM: a bucket never exceeds the mask.
def and_mask_lt
def bucket_ltw
def bucket_ltTHEOREM: with mask = 2^k - 1 (k low bits) the bucket indexes a table of 2^k.

def dm_e2
def dm_l2
def dm_eqv == (v / n) n + v mod n (Mathlib Nat.div_add_mod)
def dm_ltv mod n < n (Mathlib Nat.mod_lt)
def div_ofthe quotient and remainder are unique
def mod_of
def add_cancelc + a == c + b gives a == b (Mathlib Nat.add_left_cancel)
def mul_cancelx c == y c with c > 0 gives x == y (Mathlib Nat.eq_of_mul_eq_mul_right)
def le_add_canceld + x <= d + y is x <= y
def le_div_g
def le_divx <= n / d is x d <= n (Mathlib Nat.le_div_iff_mul_le)
def zsub
def sub_cancel_l
def mul_sub(x - y) c == x c - y c (Mathlib Nat.mul_sub_right_distrib)
def absorb(q n + r) mod n == r mod n (Mathlib Nat.mul_add_mod)