~/bend-docscommunity

proofs/math/typed/width.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as Width

6 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/logic.bend as L
import ../natural/arith.bend as NR

Definitions

def lt_half source · line 15 · raw

@+n:Nat -> @+m:Nat -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n), m) == Nat.is_lt(n, Nat.double(m)) : Bool}

half(n) < m exactly when n < 2m

def fits_lt source · line 31 · raw

@+k:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) == Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) : Bool}

fits(k, n) is n < 2^k

def hb source · line 45 · raw

@+n:Nat -> {n == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n))) : Nat}

def half_dbl source · line 55 · raw

@+r:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(Nat.add(r, Nat.double(x))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(r), x) : Nat}

def bit_dbl source · line 72 · raw

@+r:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(Nat.add(r, Nat.double(x))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(r) : Nat}

def low_high source · line 91 · raw

@+k:Nat -> @+n:Nat -> {n == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n))) : Nat}

def bit_le1 source · line 103 · raw

@+n:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n), 1n) == True{} : Bool}

def le_add_r source · line 112 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

def low_lt source · line 116 · raw

@+k:Nat -> @+n:Nat -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool}

def low_uniq source · line 132 · raw

@+k:Nat -> @+r:Nat -> @+q:Nat -> @+hr:{Nat.is_lt(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q))) == r : Nat}

r < 2^k: low(k, r + shift(k, q)) == r and high(k, r + shift(k, q)) == q

def high_uniq source · line 148 · raw

@+k:Nat -> @+r:Nat -> @+q:Nat -> @+hr:{Nat.is_lt(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q))) == q : Nat}

def shift_zero source · line 163 · raw

@+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0n) == 0n : Nat}

def shift_add source · line 170 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(x, y)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y)) : Nat}

def shift_one source · line 177 · raw

@+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 1n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) : Nat}

def shift_comp source · line 184 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.add(a, b), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, x)) : Nat}

def shift_mono source · line 191 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y)) == True{} : Bool}

def shift_pow2 source · line 199 · raw

@+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(Nat.add(a, b)) : Nat}

shift(a, 2^b) == 2^(a + b)

def two_limb_lt source · line 207 · raw

@+k:Nat -> @+j:Nat -> @+r:Nat -> @+x:Nat -> @+hr:{Nat.is_lt(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hx:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> {Nat.is_lt(Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(Nat.add(k, j))) == True{} : Bool}

r < 2^k, x < 2^j: r + shift(k, x) < 2^(k + j)

def lt_of_fits source · line 216 · raw

@+k:Nat -> @+r:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> {Nat.is_lt(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool}

def fits_of_lt source · line 219 · raw

@+k:Nat -> @+r:Nat -> @+h:{Nat.is_lt(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool}

def low_u source · line 222 · raw

@+k:Nat -> @+r:Nat -> @+q:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q))) == r : Nat}

def high_u source · line 225 · raw

@+k:Nat -> @+r:Nat -> @+q:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q))) == q : Nat}

def low_fits source · line 228 · raw

@+k:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, n)) == True{} : Bool}

def limbs_fit source · line 232 · raw

@+k:Nat -> @+j:Nat -> @+r:Nat -> @+x:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(j, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, j), Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x))) == True{} : Bool}

r fits k bits, x fits j bits: r + shift(k, x) fits k + j bits

def unfit_shift source · line 236 · raw

@+k:Nat -> @+r:Nat -> @+qp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 1n+qp))) == False{} : Bool}

shift(k, q) with q >= 1 does not fit k bits added to anything

def shift_ge source · line 240 · raw

@+k:Nat -> @+x:Nat -> {Nat.is_le(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x)) == True{} : Bool}

def unfit_one source · line 248 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one))) == False{} : Bool}

with a symbolic one == 1 (so no closed 2^k appears where these are used)

def lt_one source · line 251 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> {Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) == True{} : Bool}

def dbl_eq0 source · line 255 · raw

@+z:Nat -> {Nat.is_eq(Nat.double(z), 0n) == Nat.is_eq(z, 0n) : Bool}

def shift_eq0 source · line 262 · raw

@+k:Nat -> @+y:Nat -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y), 0n) == Nat.is_eq(y, 0n) : Bool}

def lt_cancel_l source · line 271 · raw

@+d:Nat -> @+x:Nat -> @+y:Nat -> {Nat.is_lt(Nat.add(d, x), Nat.add(d, y)) == Nat.is_lt(x, y) : Bool}

def lt_cancel_r source · line 278 · raw

@+x:Nat -> @+y:Nat -> @+s:Nat -> {Nat.is_lt(Nat.add(x, s), Nat.add(y, s)) == Nat.is_lt(x, y) : Bool}

def lt_hi source · line 283 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+h:{Nat.is_lt(y1, y2) == True{} : Bool} -> {Nat.is_lt(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) == True{} : Bool}

y1 < y2: x1 + shift(k, y1) < x2 + shift(k, y2)

def lt_limbs_c source · line 292 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> @+c:Bool -> @+d:Bool -> @+hc:{Nat.is_lt(y1, y2) == c : Bool} -> @+hd:{Nat.is_eq(y1, y2) == d : Bool} -> {Bool.or(c, Bool.and(d, Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) : Bool}

def lt_limbs source · line 305 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> {Bool.or(Nat.is_lt(y1, y2), Bool.and(Nat.is_eq(y1, y2), Nat.is_lt(x1, x2))) == Nat.is_lt(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) : Bool}

def eq_limbs_f source · line 308 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+d1:Bool -> @+d2:Bool -> @+h1:{Nat.is_eq(x1, x2) == d1 : Bool} -> @+h2:{Nat.is_eq(y1, y2) == d2 : Bool} -> @+he:{Nat.is_eq(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) == False{} : Bool} -> {Bool.and(d1, d2) == False{} : Bool}

def eq_limbs_c source · line 320 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) == c : Bool} -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == c : Bool}

def eq_limbs source · line 332 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> {Bool.and(Nat.is_eq(x1, x2), Nat.is_eq(y1, y2)) == Nat.is_eq(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) : Bool}

def bit_mod source · line 337 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n) == Nat.mod(n, 2n) : Nat}

def odd_limb source · line 346 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, y)), 2n) == Nat.mod(x, 2n) : Nat}

def shift_dbl source · line 351 · raw

@+k:Nat -> @+z:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.double(z)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, z)) : Nat}

def dbl_mul source · line 358 · raw

@+x:Nat -> @+y:Nat -> {Nat.double(Nat.mul(x, y)) == Nat.mul(x, Nat.double(y)) : Nat}

def shift_mul source · line 361 · raw

@+k:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x) == Nat.mul(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 1n)) : Nat}

def half_limbs source · line 369 · raw

@+p:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, y))) == Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(x), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(p, one))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(y))) : Nat}

half(x + shift(1 + p, y)) == half(x) + bit(y) shift(p, one) + shift(1 + p, half(y))

def fits_one source · line 379 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool}

def unfit_nz source · line 384 · raw

@+k:Nat -> @+r:Nat -> @+q:Nat -> @+hq:{Nat.is_eq(q, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q))) == False{} : Bool}

a nonzero multiple of 2^k added: does not fit k bits

def shift_mul_l source · line 393 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x), y) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(x, y)) : Nat}

def shift_mul_r source · line 397 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mul(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(x, y)) : Nat}

def low_add_shift source · line 400 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, x) : Nat}

def expand_k source · line 406 · raw

@+k:Nat -> @+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> {Nat.mul(Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, ah)), Nat.add(bl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(al, bh))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(ah, bl)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(ah, bh))))) : Nat}

def mul_k source · line 410 · raw

@+k:Nat -> @+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+t:Nat -> @+kc:Nat -> @+e:{Nat.add(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, kc)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat} -> {Nat.mul(Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, ah)), Nat.add(bl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(kc, Nat.mul(ah, bh))))) : Nat}

(al + 2^k ah)(bl + 2^k bh) == al bl + 2^k t + 2^(2k) (kc + ah bh) when al bh + ah bl == t + 2^k kc

def low_fit source · line 413 · raw

@+k:Nat -> @+r:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, r) == r : Nat}

def pow2_sq source · line 417 · raw

@+k:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(Nat.add(k, k)) : Nat}

def shift_mul_one source · line 420 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x) == Nat.mul(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) : Nat}

def shift_lt source · line 423 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == True{} : Bool}

def high_add_shift source · line 432 · raw

@+k:Nat -> @+x:Nat -> @+z:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, z))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, x), z) : Nat}

def high_comp source · line 438 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(Nat.add(b, a), n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(b, n)) : Nat}

def high_div source · line 446 · raw

@+k:Nat -> @+n:Nat -> @+pp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) == 1n+pp : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n) == Nat.div(n, 1n+pp) : Nat}

high(k, n) is n div 2^k, low(k, n) is n mod 2^k

def low_shift source · line 455 · raw

@+s:Nat -> @+t:Nat -> @+y:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(s, t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(s, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(t, y)) : Nat}

low(s + t, shift(s, y)) == shift(s, low(t, y))

def sub_lt_sub source · line 463 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> @+hc:{Nat.is_le(c, a) == True{} : Bool} -> {Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}

a < b, c <= a: a - c < b - c