bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def nstrip
def nba
def nbd
def nsmthe U64 loop's Small test on the values (both below 2^48, a at least 2^16): the loop then returns gcd(a, d) at once.
def nbloop
def ndbl
def nev2
def ntw
def nbg_b
def nbg_a
def nrb
def nbin
def not_odd_rnot odd is even
def not_odd
def strip_gcda odd: gcd(a, strip(x)) = gcd(a, x), whatever the fuel
def pos_absurd1
def dlt_inv_b
def double_lt_inv2u < 2v gives u < v
def div2_le
def half_posan even positive x = 2 (x / 2) has x / 2 > 0
def strip_oddwith fuel f and x < 2^f, stripping reaches an odd number
def strip_lestripping never grows
def mod2_double
def odd_true
def odd_pos
def double_sub
def odd_subodd a - odd s is even
def mul_pos
def bl_zero
def half_bounda (1 + kp) < 2^g from a (2 + 2 kp) < 2^(1 + g)
def strip_evenstrip(2 (1 + kp)) <= 1 + kp
def bl_case
def bl_stepone step of the loop, from the induction hypothesis for fuel g
def bl_sma small pair ends the loop with its gcd; otherwise it steps
def blthe loop from (a odd, 2k) with a * 2k < 2^f and f <= 140 computes gcd(a, 2k)
def mul_lt_sq
def bf_case
def bf_sm
def bfirsta odd, b > 0, a b < 2^139: the loop computes gcd(a, b)
def ev_ta
def ev_tb
def ev_fb
def add_self
def gcd_twicegcd(2a, 2b) = gcd(a, b) + gcd(a, b)
def exit_gcdthe exit: gcd(strip a, b) = gcd(a, b) when a or b is odd
def tw_exit
def tw_case
def twhalving while both are even: ntw computes 2^c gcd(a, b) (as c doublings)
def top_r
def nbin_gcdthe binary gcd of a, b < 2^w (w + w <= 139) is gcd(a, b)