bend-collections-laws-math
Releases (1)
-
1.0.0.0 indexed
Definitions (5,526)
proofs/math/natural/proof.bend
- def isqrt_le
- def isqrt_lt_succ
- def iroot_done
- def iroot_value
- def iroot_le
- def iroot_lt_succ
- def zero_degree
- def ilog_done
- def ilog_value
- def pow_le
- def lt_pow_succ
- def ilog_zero
- def small_base
- def bit_length_lt
- def bit_length_le
- def pow_mod_value
- def pow_mod_zero_modulus
- def inverse
- def reduced
- def factor_partsthe shared factor g >= 2 and its two quotients, as dvd pairs
- def not_coprime
- def inverse_zero_modulus
- def divmod_value
- def euclid
- def rem_lt
- def zero_divisor
- def clamp_value
- def clamp_ge
- def clamp_le
- def clamp_id
- def domain
proofs/math/natural/roots.bend
- def pow_pos
- def le_mul_posx <= x y for y > 0
- def pow_le_casethe division-guarded loop computes (acc r) r^j <= n
- def root_le_okroot_le(n, k, r) is r^k <= n
- def two_mulx 2 == x + x
- def lo_lt_midlo + 1 < hi gives lo < (lo + hi) / 2
- def mid_lt_hilo < hi gives (lo + hi) / 2 < hi
- def lt_subb < c <= a gives a - c < a - b
- def lt_sub2a < b and c <= a give a - c < b - c
- def sub_poslo < hi gives 0 < hi - lo
- def root_okthe answer r: r^k <= n < (r + 1)^k, through root_le
- def no_fuel
- def done_oklo + 1 >= hi with lo < hi: the interval is [lo, lo + 1)
- def shrinkthe interval shrinks: a step fits in the remaining fuel
- def search_ok
- def search_top
- def pow2_add2^(x + y) == 2^x 2^y
- def pow_pow2(2^a)^k == 2^(k a)
- def bl_leL <= k (1 + L / k)
- def hi_boundn < (2^(1 + L/k))^k
- def hi_pos
- def root_top
- def ok_le
- def ok_lt
- def iroot_k_ok
- def iroot_doneiroot(n, k) == Done{r} with r^k <= n < (r + 1)^k for k >= 1, Domain for k == 0
- def iroot_zero
- def iroot_le
- def lt_succ_iroot
proofs/math/natural/sqrtn.bend
- def succ_mul_succ(1 + u)(1 + v) == 1 + ((u + v) + u v)
- def le_add2a <= b and c <= d give a + c <= b + d
- def add_two(1 + x) + (1 + y) == 2 + (x + y)
- def prod_leu + v <= 2 w gives u v <= w w
- def stop_sq
- def le_zero
- def iter_sq
- def step_lt
- def step_any
- def iter_lt
- def g0_bound
- def isqrt_leisqrt(n)^2 <= n (Mathlib Nat.sqrt_le')
- def lt_succ_isqrtn < (isqrt(n) + 1)^2 (Mathlib Nat.lt_succ_sqrt')
proofs/math/number/bitcount.bend
- def half_div2
- def ones_zero
- def gothe loop adds the ones of its fuel's worth of bits
- def bit_count_value
proofs/math/number/egcd.bend
- def up_gcd
- def gcd_go
- def egcd_gcd
- def qby(q b) y == b (q y)
- def spread(q b + r) y == b (q y) + r y
- def alg_poschild b x == g + r y gives b (x + q y) == g + (q b + r) y
- def alg_negchild r y == g + b x gives (q b + r) y == g + b (x + q y)
- def basethe base case: a * 1 == a + b * 0
- def up_sign
- def up_bezone level up: from the child's identity for (b, r) to the parent's for (a, b), a == q b + r
- def splita == (a div b) b + a mod b
- def bez_go
- def egcd_bezout