bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def found_go
def le_cis_lt(a, b) is is_le(a + 1, b)
def lt_iff_c
def lt_iff
def found_one
def found
def not_value_oneUA.not_value with the unit kept open (n is 32 at the use)
def fuel_ok
def fuel_ok22^32 stays C.shift(32, one) for a symbolic one: with one == 1n the checker would expand the closed 2^32 in unary
def beyond
def none_go
def none_one
def none

def sub_big
def sub_splitd < n: n - d == 1 + (n - (d + 1))
def lt_sq2 <= d: d < d * d
def le_step
def at_ca d with lo <= e < lo + k, where nodiv(k, n, lo) holds, does not divide n
def nodiv_at
def and_true
def and_assocnodiv(1 + k, n, d) adds the test of d + k
def snoc
def mul0
def mul1
def c_smalln == q e with q >= 2 and q < d would divide n, which nodiv(dq, n, 2) rules out
def c_big...
def c_two
def contrae divides n with d <= e < n, d * d > n and no divisor in [2, d): impossible
def lt_add1e < e + (1 + p)
def head_c
def bigevery e in [2 + eq, 2 + eq + k) with d <= e, e + k <= n: none divides n
def stopthe stop at d * d > n: nothing in [d, n) divides n
def belowd * d <= n: d < n
def loop
def is_prime_value