~/bend-docscommunity

proofs/math/typed/u32int.bend checks

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

27 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/generic.bend as SG
import ../../../spec/math/natural.bend as NS
import ../../../src/math/generic.bend as G
import ../../../src/math/num.bend as NM
import ../../../src/math/natural.bend as M
import ../../../src/math/instances.bend as I
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./u32.bend as U32P
import ./u32laws.bend as LW
import ./u32mont.bend as MO
import ../../../src/math/w64.bend as X
import ./natfuel.bend as NF
import ./combnat.bend as CN
import ../../lib/arith.bend as AR2
import ../natural/fact.bend as FA
import ../natural/roots.bend as RT
import ../../../src/math/pow2.bend as P2
import ../pow2/pow2.bend as PP
import ../../../spec/math/natural.bend as S
import ../natural/inverse.bend as IV
import ../natural/proof.bend as NP

Definitions

def v source · line 36 · raw

@+x:U32 -> Nat

def of source · line 39 · raw

@+n:Nat -> U32

def as_of source · line 43 · raw

@+x:U32 -> @+n:Nat -> @+h:{v(x) == n : Nat} -> {x == of(n) : U32}

x is the U32 of its value

def true_ne_false source · line 46 · raw

@+h:{True{} == False{} : Bool} -> Empty

def isqrt_agrees source · line 51 · raw

@+n:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Isqrt.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, n)

def abs_identity source · line 54 · raw

@+x:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Abs.identity(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x)

def dm source · line 59 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{b}) == c : Bool} -> @+nb:Nat -> @+hnb:{v(b) == nb : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.divmod_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, a, b, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift_qr(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.divmod(v(a), nb)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.QuotRem<U32>>}

def divmod_agrees source · line 77 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.DivMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def lt_of source · line 82 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{a, b}) == c : Bool} -> {Nat.is_lt(v(a), v(b)) == c : Bool}

def min_c source · line 85 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{b, a}) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, b, a) == of(Nat.min(v(a), v(b))) : U32}

def min_agrees source · line 92 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Min.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def max_c source · line 95 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{a, b}) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, b, a) == of(Nat.max(v(a), v(b))) : U32}

def max_agrees source · line 102 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Max.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def max_val_c source · line 105 · raw

@+x:U32 -> @+lo:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{x, lo}) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pick(U32, c, lo, x)) == Nat.max(v(x), v(lo)) : Nat}

def zero_v source · line 112 · raw

{v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.ZeroOp{})) == 0n : Nat}

def one_v source · line 115 · raw

{v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{})) == 1n : Nat}

def sign_b source · line 118 · raw

@+x:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.ZeroOp{})}) == c : Bool} -> @+hz:{Nat.is_lt(0n, v(x)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sign_below(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}

def sign_a source · line 126 · raw

@+x:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.ZeroOp{}), x}) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sign_above(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}

def sign_agrees source · line 136 · raw

@+x:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sign.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, x)

def clamp_d source · line 139 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.clamp_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, lo, hi, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.clamp_ok(v(x), v(lo), v(hi), c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def clamp_c source · line 150 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{hi, lo}) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.clamp_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, lo, hi, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.clamp(v(x), v(lo), v(hi))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def clamp_agrees source · line 154 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Clamp.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, x, lo, hi)

def gcd_sim source · line 159 · raw

@+f:Nat -> @+a:U32 -> @+b:U32 -> @+cz:Bool -> @+nb:Nat -> @+hcz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{b}) == cz : Bool} -> @+hnb:{v(b) == nb : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, a, (b, cz))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(f, v(a), nb) : Nat}

def gcd_val_k source · line 178 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> @+b:U32 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(v(a), v(b)) : Nat}

def gcd_val source · line 182 · raw

@+a:U32 -> @+b:U32 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(v(a), v(b)) : Nat}

def gcd_agrees source · line 185 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Gcd.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, b)

def vals source · line 190 · raw

@xs:List<&2, U32> -> List<&2, Nat>

def gall source · line 193 · raw

@+xs:List<&2, U32> -> @+acc:U32 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd_all_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, xs, acc)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_all_go(vals(xs), v(acc)) : Nat}

def gcd_all_agrees source · line 201 · raw

@+xs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.GcdAll.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, xs)

def mo_of source · line 207 · raw

@+q:U32 -> @+b:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(q), v(b)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{q, b}) == Bool.not(c) : Bool}

def cm source · line 211 · raw

@+q:U32 -> @+b:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(q), v(b)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.cmul(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, q, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, n) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def gpos_d source · line 227 · raw

@+ap:Nat -> @+b:Nat -> @d:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(1n+ap, b), 1n+ap) -> @+g:Nat -> @+hg:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(1n+ap, b) == g : Nat} -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(1n+ap, b), 0n) == False{} : Bool}

def gpos source · line 238 · raw

@+ap:Nat -> @+b:Nat -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(1n+ap, b), 0n) == False{} : Bool}

gcd of a positive number is positive

def iz source · line 241 · raw

@+a:U32 -> @+n:Nat -> @+h:{v(a) == n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{a}) == Nat.is_eq(n, 0n) : Bool}

def lcmc source · line 244 · raw

@+a:U32 -> @+b:U32 -> @+c:Bool -> @+na:Nat -> @+nb:Nat -> @+hc:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{a}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{b})) == c : Bool} -> @+hna:{v(a) == na : Nat} -> @+hnb:{v(b) == nb : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.lcm_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, a, b, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(na, nb)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def lcm_checked source · line 268 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Lcm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, a, b)

def lall_fail source · line 273 · raw

@xs:List<&2, U32> -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.lcm_all_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, xs, Fail{e}) == Fail{e} : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def lgo_false source · line 280 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lcm_go(32n, xs, acc, False{}) == (acc, False{}) : Pair(Nat, Bool)}

def lall source · line 288 · raw

@+xs:List<&2, U32> -> @+r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32> -> @+n:Nat -> @+c:Bool -> @+hr:{r == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked_pick(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, n, c) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.lcm_all_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, xs, r) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.prefix_fin(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lcm_go(32n, vals(xs), n, c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

the fold on an accumulator r == checked(n) (c == fits(32, n))

def lcm_all_checked source · line 301 · raw

@+xs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.LcmAll.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, xs)

def cmul_rel source · line 306 · raw

@+q:U32 -> @+x:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(q), v(x)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.cmul(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, q, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}

def pal source · line 316 · raw

@+xs:List<&2, U32> -> @+r:Maybe<&2, U32> -> @+n:Nat -> @+c:Bool -> @+hr:{r == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.prod_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, xs, r)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.prefix_fin(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.prod_go(32n, vals(xs), n, c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def prod_checked source · line 332 · raw

@+xs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Prod.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, xs)

def ao_of source · line 337 · raw

@+q:U32 -> @+b:U32 -> @+n:Nat -> @+hn:{Nat.add(v(q), v(b)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{q, b}) == Bool.not(c) : Bool}

def cadd_rel source · line 341 · raw

@+q:U32 -> @+x:U32 -> @+n:Nat -> @+hn:{Nat.add(v(q), v(x)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.cadd(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, q, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}

def unfit_mono source · line 352 · raw

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

a value that does not fit stays unfit when it grows

def sal source · line 356 · raw

@+xs:List<&2, U32> -> @+r:Maybe<&2, U32> -> @+n:Nat -> @+c:Bool -> @+hr:{r == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sum_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, xs, r)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, Nat.add(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.lsum(vals(xs)))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def sum_checked source · line 380 · raw

@+xs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sum.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, xs)

def blsim source · line 385 · raw

@+f:Nat -> @+k:Nat -> @+n:U32 -> @+cz:Bool -> @+nn:Nat -> @+hcz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{n}) == cz : Bool} -> @+hnn:{v(n) == nn : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bit_length_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, k, (n, cz)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length_go(f, nn, k) : Nat}

def bit_length_k source · line 400 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+n:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bit_length(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(n)) : Nat}

def bit_length_agrees source · line 404 · raw

@+n:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.BitLength.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, n)

def pmo_lt source · line 409 · raw

@+mp:Nat -> @+d:Nat -> @+base:Nat -> @+acc:Nat -> @+ha:{Nat.is_lt(acc, 1n+mp) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+mp, d, base, acc), 1n+mp) == True{} : Bool}

def lt_m source · line 416 · raw

@+x:U32 -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+h:{Nat.is_lt(v(x), 1n+mp) == True{} : Bool} -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}

def mmb_v source · line 419 · raw

@+m:U32 -> @+b:U32 -> @+acc:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+hb:{Nat.is_lt(v(b), 1n+mp) == True{} : Bool} -> @+ha:{Nat.is_lt(v(acc), 1n+mp) == True{} : Bool} -> @+d:Nat -> @+o:Bool -> @+hd:{Nat.is_lt(d, 2n) == True{} : Bool} -> @+ho:{o == Nat.is_eq(d, 1n) : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.mm_bit(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, o, m, b, acc)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+mp, d, v(b), v(acc)) : Nat}

def pmsim source · line 432 · raw

@+f:Nat -> @+m:U32 -> @+b:U32 -> @+acc:U32 -> @+e:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+hb:{Nat.is_lt(v(b), 1n+mp) == True{} : Bool} -> @+ha:{Nat.is_lt(v(acc), 1n+mp) == True{} : Bool} -> @+ez:Bool -> @+ne:Nat -> @+hez:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{e}) == ez : Bool} -> @+hne:{v(e) == ne : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, m, b, acc, (e, ez))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f, 1n+mp, ne, v(b), v(acc)) : Nat}

def pm_rem source · line 457 · raw

@+x:U32 -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{x, m})) == Nat.mod(v(x), 1n+mp) : Nat}

def pm_gen source · line 463 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+b:U32 -> @+e:U32 -> @+m:U32 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 140n, m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{b, m}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), m}), (e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{e})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}

the generic MulMod loop (mont32_ok(m) False)

def pm_mont source · line 477 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+b:U32 -> @+e:U32 -> @+m:U32 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont32_ok(m) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.PowMod{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{b, m}), e, m})) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}

32-bit Montgomery multiplication (mont32_ok(m) True)

def pm_pick source · line 481 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+b:U32 -> @+e:U32 -> @+m:U32 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont32_ok(m) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_pick(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, b, e, m, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}

def pm_top source · line 488 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+b:U32 -> @+e:U32 -> @+m:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{m}) == c : Bool} -> @+nm:Nat -> @+hnm:{v(m) == nm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, b, e, m, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod(v(b), v(e), nm)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def powmod_agrees source · line 501 · raw

@+b:U32 -> @+e:U32 -> @+m:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.PowMod.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, b, e, m)

def nlt source · line 506 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {Nat.is_lt(a, b) == Nat.is_lt(na, nb) : Bool}

def ltv source · line 509 · raw

@+a:U32 -> @+b:U32 -> @+na:Nat -> @+nb:Nat -> @+ha:{v(a) == na : Nat} -> @+hb:{v(b) == nb : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{a, b}) == Nat.is_lt(na, nb) : Bool}

def nsub source · line 512 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {Nat.sub(a, b) == Nat.sub(na, nb) : Nat}

def nadd source · line 515 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {Nat.add(a, b) == Nat.add(na, nb) : Nat}

def mv source · line 518 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> {Nat.is_lt(1n+mp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool}

def fits32 source · line 521 · raw

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

def lt_mn source · line 524 · raw

@+x:U32 -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+nx:Nat -> @+hx:{v(x) == nx : Nat} -> @+h:{Nat.is_lt(nx, 1n+mp) == True{} : Bool} -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}

def subv source · line 527 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+s0:U32 -> @+x:U32 -> @+ns0:Nat -> @+nx:Nat -> @+hs0:{v(s0) == ns0 : Nat} -> @+hx:{v(x) == nx : Nat} -> @+hb0:{Nat.is_lt(ns0, 1n+mp) == True{} : Bool} -> @+hbx:{Nat.is_lt(nx, 1n+mp) == True{} : Bool} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{s0, x}) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.submod(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, m, s0, x, c)) == Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp) : Nat}

def stepv source · line 544 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+q:U32 -> @+s0:U32 -> @+s1:U32 -> @+nq:Nat -> @+ns0:Nat -> @+ns1:Nat -> @+hq:{v(q) == nq : Nat} -> @+hs0:{v(s0) == ns0 : Nat} -> @+hs1:{v(s1) == ns1 : Nat} -> @+hb0:{Nat.is_lt(ns0, 1n+mp) == True{} : Bool} -> @+hb1:{Nat.is_lt(ns1, 1n+mp) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_step(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, m, q, s0, s1)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_step(1n+mp, nq, ns0, ns1) : Nat}

def pv source · line 553 · raw

@p:Pair(U32, U32) -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout

def bzeq source · line 557 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.BZ{a, b} == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.BZ{na, nb} : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout}

def or_true source · line 560 · raw

@+x:Bool -> {Bool.or(x, True{}) == True{} : Bool}

def invsim source · line 567 · raw

@+f:Nat -> @+k:Nat -> @+hk:{k == 32n : Nat} -> @+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+r0:U32 -> @+s0:U32 -> @+s1:U32 -> @+r1:U32 -> @+nr0:Nat -> @+ns0:Nat -> @+ns1:Nat -> @+hr0:{v(r0) == nr0 : Nat} -> @+hs0:{v(s0) == ns0 : Nat} -> @+hs1:{v(s1) == ns1 : Nat} -> @+hb0:{Nat.is_lt(ns0, 1n+mp) == True{} : Bool} -> @+cz:Bool -> @+nr1:Nat -> @+hcz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{r1}) == cz : Bool} -> @+hr1:{v(r1) == nr1 : Nat} -> @+hb1:{Bool.or(Nat.is_eq(nr1, 0n), Nat.is_lt(ns1, 1n+mp)) == True{} : Bool} -> {pv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, m, r0, s0, s1, (r1, cz))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(f, 1n+mp, nr0, ns0, nr1, ns1) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout}

def fin2 source · line 588 · raw

@+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+s:U32 -> @+sn:Nat -> @+hs:{v(s) == sn : Nat} -> @+cb:Bool -> @+gn:Nat -> @+hcb:{Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))) == cb : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_one(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, m, s, cb) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_fin(1n+mp, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.BZ{gn, sn})) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def finsim source · line 603 · raw

@+m:U32 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @p:Pair(U32, U32) -> @+bz:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout -> @+h:{pv(p) == bz : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_fin(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, m, p) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_fin(1n+mp, bz)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def lt1_eq source · line 612 · raw

@+x:Nat -> @+h:{Nat.is_lt(x, 1n) == True{} : Bool} -> {Nat.is_eq(x, 0n) == True{} : Bool}

def hb_init source · line 619 · raw

@+mp:Nat -> @+a:Nat -> {Bool.or(Nat.is_eq(Nat.mod(a, 1n+mp), 0n), Nat.is_lt(1n, 1n+mp)) == True{} : Bool}

def inv_top source · line 626 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> @+m:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{m}) == c : Bool} -> @+nm:Nat -> @+hnm:{v(m) == nm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, a, m, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.mod_inverse(v(a), nm)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def modinv_agrees source · line 643 · raw

@+a:U32 -> @+m:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.ModInverse.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, a, m)

def nle source · line 648 · raw

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

def nmul source · line 655 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {Nat.mul(a, b) == Nat.mul(na, nb) : Nat}

def lev source · line 659 · raw

@+x:U32 -> @+y:U32 -> @+nx:Nat -> @+ny:Nat -> @+hx:{v(x) == nx : Nat} -> @+hy:{v(y) == ny : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, x, y) == Nat.is_le(nx, ny) : Bool}

le(x, y) on U32 is is_le on the values

def ilsim source · line 662 · raw

@+f:Nat -> @+q:U32 -> @+b:U32 -> @+k:Nat -> @+p:U32 -> @+nn:Nat -> @+bq:Nat -> @+np:Nat -> @+hq:{v(q) == Nat.div(nn, 2n+bq) : Nat} -> @+hb:{v(b) == 2n+bq : Nat} -> @+hp:{v(p) == np : Nat} -> @+K:Nat -> @+hK:{K == 32n : Nat} -> @+hn:{Nat.is_lt(nn, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool} -> @+up:Bool -> @+hup:{up == Nat.is_le(np, Nat.div(nn, 2n+bq)) : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ilog_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, q, b, k, p, up) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(f, nn, 2n+bq, k, np, up) : Nat}

def or_false_r source · line 680 · raw

@+x:Bool -> @+y:Bool -> @+h:{Bool.or(x, y) == False{} : Bool} -> {y == False{} : Bool}

def ilog_fin source · line 687 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+b:U32 -> @+nb:Nat -> @+hb:{v(b) == nb : Nat} -> @+hl:{Nat.is_lt(nb, 2n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ilog_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, b, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_ok(v(n), nb, False{})) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def ilog_top source · line 709 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+b:U32 -> @+bad:Bool -> @+hN:{Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n)) == bad : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ilog_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, b, bad) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_ok(v(n), v(b), bad)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>}

def two_v source · line 716 · raw

{v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Add{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{})})) == 2n : Nat}

def ilog_agrees source · line 722 · raw

@+n:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Ilog.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, n, b)

def FR source · line 732 · raw

@ok:Bool -> @a:U32 -> @x:Nat -> Type

the value when the flag says it fits

def not_not source · line 739 · raw

@+c:Bool -> {Bool.not(Bool.not(c)) == c : Bool}

def fr_mul source · line 746 · raw

@+a:U32 -> @+x:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(a), v(x)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> FR(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, x})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Mul{a, x}), n)

def ok_mul source · line 757 · raw

@+a:U32 -> @+x:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(a), v(x)) == n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, x})) : Bool}

the flag after a checked multiply is fits(product)

def fk source · line 760 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+x:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, x) == True{} : Bool} -> {Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool}

def succ_le source · line 764 · raw

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

def plus1 source · line 773 · raw

@+x:Nat -> {Nat.add(x, 1n) == 1n+x : Nat}

def inc_v source · line 777 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+i:U32 -> @+n:U32 -> @+ni:Nat -> @+nn:Nat -> @+hi:{v(i) == ni : Nat} -> @+hn:{v(n) == nn : Nat} -> @+hlt:{Nat.is_lt(ni, nn) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inc(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, i)) == 1n+ni : Nat}

inc(i) for i < n is i + 1

def factsim source · line 784 · raw

@+f:Nat -> @+i:U32 -> @+n:U32 -> @+a:U32 -> @+ni:Nat -> @+nn:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 32n : Nat} -> @+hi:{v(i) == ni : Nat} -> @+hn:{v(n) == nn : Nat} -> @+hmono:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(ni), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(nn)) == True{} : Bool} -> @+hf:{Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(ni)) == ok : Bool} -> @ha:FR(ok, a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(ni)) -> @+hmore:{more == Nat.is_lt(ni, nn) : Bool} -> @+hcn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(nn)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fact_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, i, n, (a, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(nn))) : Maybe<&2, U32>}

def okfits source · line 812 · raw

@+x:Nat -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(x))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked_pick(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, x, c) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def fact_top source · line 819 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, n)

def factorial_checked source · line 827 · raw

@+n:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, n)

def pmon source · line 832 · raw

@+nn:Nat -> @+j:Nat -> @+r:Nat -> @+k0:Nat -> @+hj:{Nat.add(j, r) == k0 : Nat} -> @+hle:{Nat.is_le(k0, nn) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, j), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, k0)) == True{} : Bool}

def le_v source · line 836 · raw

@+a:U32 -> @+b:U32 -> @+na:Nat -> @+nb:Nat -> @+ha:{v(a) == na : Nat} -> @+hb:{v(b) == nb : Nat} -> @+h:{Nat.is_le(na, nb) == True{} : Bool} -> {Nat.is_le(v(a), v(b)) == True{} : Bool}

def permsim source · line 840 · raw

@+f:Nat -> @+k:U32 -> @+m:U32 -> @+a:U32 -> @+nn:Nat -> @+j:Nat -> @+r:Nat -> @+k0:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 32n : Nat} -> @+hkr:{v(k) == r : Nat} -> @+hm:{v(m) == Nat.sub(nn, j) : Nat} -> @+hj:{Nat.add(j, r) == k0 : Nat} -> @+hle:{Nat.is_le(k0, nn) == True{} : Bool} -> @+hf:{Nat.is_le(1n+K, Nat.add(f, j)) == True{} : Bool} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, j)) == ok : Bool} -> @ha:FR(ok, a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, j)) -> @+hmore:{more == Bool.not(Nat.is_eq(r, 0n)) : Bool} -> @+hcn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, k0)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.perm_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, k, m, (a, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, k0))) : Maybe<&2, U32>}

def perm_top source · line 884 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+k:U32 -> @+big:Bool -> @+hbig:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{n, k}) == big : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.perm_big(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, k, big) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(v(n), v(k))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def perm_checked source · line 901 · raw

@+n:U32 -> @+k:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Perm.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, n, k)

def fv source · line 907 · raw

@ok:Bool -> @+y:Nat -> @+x:Nat -> Nat

y when ok, else x: {fv(ok, v(a), x) == x} says v(a) == x when ok

def mode source · line 915 · raw

@md:Bool -> @+x:Nat -> Bool

md: every value >= 1, or every value <= 1 (the base 0 case)

def small_fits source · line 922 · raw

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

def small_mul source · line 931 · raw

@+x:Nat -> @+y:Nat -> @+hx:{Nat.is_le(x, 1n) == True{} : Bool} -> @+hy:{Nat.is_le(y, 1n) == True{} : Bool} -> {Nat.is_le(Nat.mul(x, y), 1n) == True{} : Bool}

def pos_of source · line 940 · raw

@+x:Nat -> @+h:{Nat.is_le(1n, x) == True{} : Bool} -> {Nat.is_lt(0n, x) == True{} : Bool}

def unfit_mul source · line 948 · raw

@+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, x) == False{} : Bool} -> @+hy:{Nat.is_le(1n, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.mul(x, y)) == False{} : Bool}

x unfit, 1 <= y: x y unfit

def unfit_mul_r source · line 951 · raw

@+x:Nat -> @+y:Nat -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, y) == False{} : Bool} -> @+hx:{Nat.is_le(1n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.mul(x, y)) == False{} : Bool}

def unfit_big source · line 955 · raw

@+x:Nat -> @+md:Bool -> @+hm:{mode(md, x) == True{} : Bool} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, x) == False{} : Bool} -> {md == True{} : Bool}

an unfit value is >= 1, so the mode is the >= 1 one

def fv_mul source · line 962 · raw

@+a:U32 -> @+x:U32 -> @+n:Nat -> @+hn:{Nat.mul(v(a), v(x)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == c : Bool} -> {fv(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, x})), v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Mul{a, x})), n) == n : Nat}

def sq_fits source · line 974 · raw

@+more:Bool -> @+b:U32 -> @+bok:Bool -> @+nb:Nat -> @+md:Bool -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, nb) == bok : Bool} -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> @+hm:{mode(md, nb) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.sqn(more, nb)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, more, b, bok) : Bool}

def sq_fv source · line 985 · raw

@+more:Bool -> @+b:U32 -> @+bok:Bool -> @+nb:Nat -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> {fv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_ok(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, more, b, bok), v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_val(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, more, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.sqn(more, nb)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.sqn(more, nb) : Nat}

def sq_mode source · line 994 · raw

@+more:Bool -> @+nb:Nat -> @+md:Bool -> @+hm:{mode(md, nb) == True{} : Bool} -> {mode(md, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.sqn(more, nb)) == True{} : Bool}

def ms_a source · line 1005 · raw

@bit:Bool -> @+a:U32 -> @+b:U32 -> U32

def ms_ok source · line 1012 · raw

@bit:Bool -> @+a:U32 -> @+aok:Bool -> @+b:U32 -> @+bok:Bool -> Bool

def ms_eq source · line 1019 · raw

@+bit:Bool -> @+b:U32 -> @+bok:Bool -> @+a:U32 -> @+aok:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.mul_st(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, bit, b, bok, (a, aok)) == (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)) : Pair(U32, Bool)}

def ms_fits source · line 1026 · raw

@+bit:Bool -> @+a:U32 -> @+aok:Bool -> @+b:U32 -> @+bok:Bool -> @+na:Nat -> @+nb:Nat -> @+md:Bool -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, na) == aok : Bool} -> @+ha:{fv(aok, v(a), na) == na : Nat} -> @+hma:{mode(md, na) == True{} : Bool} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, nb) == bok : Bool} -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> @+hmb:{mode(md, nb) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.msn(bit, na, nb)) == ms_ok(bit, a, aok, b, bok) : Bool}

def ms_fv source · line 1039 · raw

@+bit:Bool -> @+a:U32 -> @+aok:Bool -> @+b:U32 -> @+bok:Bool -> @+na:Nat -> @+nb:Nat -> @+ha:{fv(aok, v(a), na) == na : Nat} -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> {fv(ms_ok(bit, a, aok, b, bok), v(ms_a(bit, a, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.msn(bit, na, nb)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.msn(bit, na, nb) : Nat}

def ms_mode source · line 1050 · raw

@+bit:Bool -> @+na:Nat -> @+nb:Nat -> @+md:Bool -> @+hma:{mode(md, na) == True{} : Bool} -> @+hmb:{mode(md, nb) == True{} : Bool} -> {mode(md, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/natfuel.msn(bit, na, nb)) == True{} : Bool}

def pw_fin source · line 1059 · raw

@+a:U32 -> @+aok:Bool -> @+na:Nat -> @+t0:Nat -> @+ct:Bool -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, na) == aok : Bool} -> @+ha:{fv(aok, v(a), na) == na : Nat} -> @+et:{na == t0 : Nat} -> @+hct:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, t0) == ct : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(aok), a) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}

def powsim source · line 1070 · raw

@+f:Nat -> @+e:Nat -> @+b:U32 -> @+bok:Bool -> @+a:U32 -> @+aok:Bool -> @+nb:Nat -> @+na:Nat -> @+t0:Nat -> @+md:Bool -> @+ct:Bool -> @+he:{Nat.is_le(e, f) == True{} : Bool} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, nb) == bok : Bool} -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> @+hmb:{mode(md, nb) == True{} : Bool} -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, na) == aok : Bool} -> @+ha:{fv(aok, v(a), na) == na : Nat} -> @+hma:{mode(md, na) == True{} : Bool} -> @+ht:{Nat.mul(na, Nat.pow(nb, e)) == t0 : Nat} -> @+hct:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, t0) == ct : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, e, b, bok, (a, aok)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}

def md_init source · line 1087 · raw

@+x:Nat -> Pair({mode(Nat.is_le(1n, x), x) == True{} : Bool}, {mode(Nat.is_le(1n, x), 1n) == True{} : Bool})

def pow_fin source · line 1095 · raw

@+x:U32 -> @+k:Nat -> @p:Pair({mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool}, {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Pow.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, x, k)

def pow_checked source · line 1104 · raw

@+x:U32 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Pow.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, x, k)

def pw_val source · line 1109 · raw

@+x:U32 -> @+k:Nat -> @p:Pair({mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool}, {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 1n+k, k, x, True{}, (0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), True{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.pow(v(x), k))), of(Nat.pow(v(x), k))) : Maybe<&2, U32>}

def rlf source · line 1115 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+P:Nat -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, P) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.root_le_fin(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(c), of(P))) == Nat.is_le(P, v(n)) : Bool}

def rl_v source · line 1125 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+k:Nat -> @+r:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.root_le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}

def imid_v source · line 1129 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+a:Nat -> @+w:Nat -> @+ha:{v(lo) == a : Nat} -> @+hh:{v(hi) == Nat.add(a, w) : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.imid(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, lo, hi)) == Nat.add(a, Nat.div(w, 2n)) : Nat}

def lt_add_r source · line 1141 · raw

@+a:Nat -> @+q:Nat -> @+h:{Nat.is_lt(0n, q) == True{} : Bool} -> {Nat.is_lt(a, Nat.add(a, q)) == True{} : Bool}

def more_v source · line 1146 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+lo:U32 -> @+hi:U32 -> @+a:Nat -> @+w:Nat -> @+ha:{v(lo) == a : Nat} -> @+hh:{v(hi) == Nat.add(a, w) : Nat} -> @+hw:{Nat.is_lt(0n, w) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inc(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, lo), hi}) == Nat.is_lt(1n, w) : Bool}

inc(lo) < lo + w as 1 < w

def srch source · line 1150 · raw

@+f:Nat -> @+n:U32 -> @+k:Nat -> @+lo:U32 -> @+hi:U32 -> @+m:U32 -> @+more:Bool -> @+hit:Bool -> @+j:Nat -> @+nlo:Nat -> @+w:Nat -> @+R:Nat -> @+K:Nat -> @+hK:{K == 32n : Nat} -> @+hlo:{v(lo) == nlo : Nat} -> @+hhi:{v(hi) == Nat.add(nlo, w) : Nat} -> @+hm:{v(m) == Nat.add(nlo, Nat.div(w, 2n)) : Nat} -> @+hR1:{Nat.is_le(Nat.pow(R, k), v(n)) == True{} : Bool} -> @+hR2:{Nat.is_lt(v(n), Nat.pow(1n+R, k)) == True{} : Bool} -> @+hl:{Nat.is_le(nlo, R) == True{} : Bool} -> @+hr:{Nat.is_lt(R, Nat.add(nlo, w)) == True{} : Bool} -> @+hmore:{more == Nat.is_lt(1n, w) : Bool} -> @+hhit:{hit == Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(w, 2n)), k), v(n)) : Bool} -> @+hw:{Nat.is_le(w, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> @+hf:{Nat.is_le(1n+j, f) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.search_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}

def iroot_big source · line 1193 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+kp:Nat -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.iroot_k(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, 2n+kp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.iroot_k(v(n), 2n+kp) : Nat}

def iroot_agrees source · line 1221 · raw

@+n:U32 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Iroot.agrees(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, n, k)

def nz_of source · line 1232 · raw

@+x:U32 -> @+n:Nat -> @+hx:{v(x) == n : Nat} -> @+h:{Nat.is_lt(0n, n) == True{} : Bool} -> {Nat.is_eq(v(x), 0n) == False{} : Bool}

def ndiv source · line 1235 · raw

@+a:Nat -> @+b:Nat -> @+na:Nat -> @+nb:Nat -> @+ha:{a == na : Nat} -> @+hb:{b == nb : Nat} -> {Nat.div(a, b) == Nat.div(na, nb) : Nat}

def quot_v source · line 1238 · raw

@+a:U32 -> @+b:U32 -> @+na:Nat -> @+nb:Nat -> @+ha:{v(a) == na : Nat} -> @+hb:{v(b) == nb : Nat} -> @+hpos:{Nat.is_lt(0n, nb) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Quot{a, b})) == Nat.div(na, nb) : Nat}

def combsim source · line 1241 · raw

@+f:Nat -> @+n:U32 -> @+i:U32 -> @+k:U32 -> @+r:U32 -> @+nn:Nat -> @+ni:Nat -> @+k0:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 32n : Nat} -> @+hn:{v(n) == nn : Nat} -> @+hi:{v(i) == ni : Nat} -> @+hk:{v(k) == k0 : Nat} -> @+h2:{Nat.is_le(Nat.double(k0), nn) == True{} : Bool} -> @+hle:{Nat.is_le(ni, k0) == True{} : Bool} -> @+hf:{Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, ni)) == ok : Bool} -> @+ha:{fv(ok, v(r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, ni)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, ni) : Nat} -> @+hmore:{more == Nat.is_lt(ni, k0) : Bool} -> @+hcn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, k0)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.comb_go(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, f, n, i, k, (r, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(U32, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, k0))) : Maybe<&2, U32>}

def min_le_a source · line 1284 · raw

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

def min_le_b source · line 1291 · raw

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

def le_add_rr source · line 1298 · 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 comb_top source · line 1302 · raw

@+K:Nat -> @+hK:{K == 32n : Nat} -> @+n:U32 -> @+k:U32 -> @+big:Bool -> @+hbig:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{n, k}) == big : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.comb_big(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, n, k, big) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(v(n), v(k))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>}

def comb_checked source · line 1336 · raw

@+n:U32 -> @+k:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Comb.checked(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_of, 32n, n, k)