~/bend-docscommunity

proofs/math/typed/u64int.bend checks

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

29 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 ./u64laws.bend as LW
import ../../../src/math/u64.bend as WU
import ./natfuel.bend as NF
import ./u64bgcd.bend as UB
import ./u64mont.bend as MO
import ../../../src/math/w64.bend as X
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 38 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

def of source · line 41 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def as_of source · line 45 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+h:{v(x) == n : Nat} -> {x == of(n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64}

x is the WU.U64 of its value

def true_ne_false source · line 48 · raw

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

def isqrt_agrees source · line 53 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Isqrt.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, n)

def abs_identity source · line 56 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Abs.identity(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, x)

def dm source · line 61 · raw

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

def divmod_agrees source · line 79 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.DivMod.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, a, b)

def lt_of source · line 84 · raw

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

def min_c source · line 87 · raw

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

def min_agrees source · line 94 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Min.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, a, b)

def max_c source · line 97 · raw

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

def max_agrees source · line 104 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Max.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, a, b)

def max_val_c source · line 107 · raw

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

def zero_v source · line 114 · raw

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

def one_v source · line 117 · raw

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

def sign_b source · line 120 · raw

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

def sign_a source · line 128 · raw

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

def sign_agrees source · line 138 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sign.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, x)

def clamp_d source · line 141 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.clamp_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, x, lo, hi, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.clamp_ok(v(x), v(lo), v(hi), c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def clamp_c source · line 152 · raw

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

def clamp_agrees source · line 156 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Clamp.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, x, lo, hi)

def gcd_sim source · line 161 · raw

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

def gcd_val_k source · line 180 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(v(a), v(b)) : Nat}

def gcd_val source · line 183 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(v(a), v(b)) : Nat}

def gcd_agrees source · line 186 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Gcd.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, a, b)

def vals source · line 191 · raw

@xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> List<&2, Nat>

def gall source · line 194 · raw

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

def gcd_all_agrees source · line 202 · raw

@+xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.GcdAll.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, xs)

def mo_of source · line 208 · raw

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

def cm source · line 212 · raw

@+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+hn:{Nat.mul(v(q), v(b)) == n : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.cmul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, q, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, n) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def gpos_d source · line 228 · 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 239 · 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 242 · raw

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

def lcmc source · line 245 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Bool -> @+na:Nat -> @+nb:Nat -> @+hc:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{a}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.lcm(na, nb)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def lcm_checked source · line 269 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Lcm.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, a, b)

def lall_fail source · line 274 · raw

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

def lgo_false source · line 281 · raw

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

def lall source · line 289 · raw

@+xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+n:Nat -> @+c:Bool -> @+hr:{r == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, n, c) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.lcm_all_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, xs, r) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.prefix_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lcm_go(64n, vals(xs), n, c)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

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

def lcm_all_checked source · line 302 · raw

@+xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.LcmAll.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, xs)

def cmul_rel source · line 307 · raw

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

def pal source · line 317 · raw

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

def prod_checked source · line 333 · raw

@+xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Prod.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, xs)

def ao_of source · line 338 · raw

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

def cadd_rel source · line 342 · raw

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

def unfit_mono source · line 353 · 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 357 · raw

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

def sum_checked source · line 381 · raw

@+xs:List<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Sum.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, xs)

def blsim source · line 386 · raw

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

def bit_length_k source · line 401 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(v(n)) : Nat}

def bit_length_agrees source · line 405 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.BitLength.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, n)

def pmo_lt source · line 410 · 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 417 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 420 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+acc:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, o, m, b, acc)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+mp, d, v(b), v(acc)) : Nat}

def pmsim source · line 433 · raw

@+f:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+acc:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{e}) == ez : Bool} -> @+hne:{v(e) == ne : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 458 · raw

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

def pm_gen source · line 464 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 140n, m, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{b, m}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Rem{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), m}), (e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 (mont_ok(m) False)

def pm_mont source · line 478 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(m) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.PowMod{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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}

Montgomery multiplication (mont_ok(m) True)

def pm_pick source · line 482 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hnm:{v(m) == 1n+mp : Nat} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(m) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_mod_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 489 · raw

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

def powmod_agrees source · line 502 · raw

@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.PowMod.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, b, e, m)

def nlt source · line 507 · 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 510 · raw

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

def nsub source · line 513 · 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 516 · 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 519 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 522 · raw

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

def lt_mn source · line 525 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 528 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{s0, x}) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.submod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, m, s0, x, c)) == Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp) : Nat}

def stepv source · line 545 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, m, q, s0, s1)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_step(1n+mp, nq, ns0, ns1) : Nat}

def pv source · line 554 · raw

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

def bzeq source · line 558 · 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 561 · raw

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

def invsim source · line 568 · raw

@+f:Nat -> @+k:Nat -> @+hk:{k == 64n : Nat} -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+r0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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.u64_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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 589 · raw

@+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:Nat -> @+hm:{v(m) == 1n+mp : Nat} -> @+s:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, m, s, cb) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_fin(1n+mp, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.BZ{gn, sn})) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def finsim source · line 604 · raw

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

def lt1_eq source · line 613 · raw

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

def hb_init source · line 620 · 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 627 · raw

@+k:Nat -> @+hk:{k == 64n : Nat} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{m}) == c : Bool} -> @+nm:Nat -> @+hnm:{v(m) == nm : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inv_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, m, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.lift(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.mod_inverse(v(a), nm)) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def modinv_agrees source · line 644 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.ModInverse.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, a, m)

def nle source · line 649 · 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 656 · 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 660 · raw

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

le(x, y) on WU.U64 is is_le on the values

def ilsim source · line 663 · raw

@+f:Nat -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 == 64n : 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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 681 · raw

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

def ilog_fin source · line 688 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+nb:Nat -> @+hb:{v(b) == nb : Nat} -> @+hl:{Nat.is_lt(nb, 2n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.ilog_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 710 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 717 · raw

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

def ilog_agrees source · line 723 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Ilog.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, n, b)

def FR source · line 733 · raw

@ok:Bool -> @a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @x:Nat -> Type

the value when the flag says it fits

def not_not source · line 740 · raw

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

def fr_mul source · line 747 · raw

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

def ok_mul source · line 758 · raw

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

the flag after a checked multiply is fits(product)

def fk source · line 761 · raw

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

def succ_le source · line 765 · 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 774 · raw

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

def inc_v source · line 778 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+i:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, i)) == 1n+ni : Nat}

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

def factsim source · line 785 · raw

@+f:Nat -> @+i:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ni:Nat -> @+nn:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 64n : 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(64n, 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(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(nn)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fact_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, i, n, (a, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(nn))) : Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def okfits source · line 813 · raw

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

def fact_top source · line 820 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, n)

def factorial_checked source · line 828 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Factorial.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, n)

def pmon source · line 833 · 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 837 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 841 · raw

@+f:Nat -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+nn:Nat -> @+j:Nat -> @+r:Nat -> @+k0:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 64n : 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(64n, 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(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, k0)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.perm_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, k, m, (a, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(nn, k0))) : Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def perm_top source · line 885 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+big:Bool -> @+hbig:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{n, k}) == big : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.perm_big(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, n, k, big) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(v(n), v(k))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def perm_checked source · line 902 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Perm.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, n, k)

def fv source · line 908 · 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 916 · raw

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

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

def small_fits source · line 923 · raw

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

def small_mul source · line 932 · 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 941 · raw

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

def unfit_mul source · line 949 · raw

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

x unfit, 1 <= y: x y unfit

def unfit_mul_r source · line 952 · raw

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

def unfit_big source · line 956 · raw

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

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

def fv_mul source · line 963 · raw

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

def sq_fits source · line 975 · raw

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

def sq_fv source · line 986 · raw

@+more:Bool -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bok:Bool -> @+nb:Nat -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> {fv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, more, b, bok), v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.sq_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_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 995 · 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 1006 · raw

@bit:Bool -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def ms_ok source · line 1013 · raw

@bit:Bool -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+aok:Bool -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bok:Bool -> Bool

def ms_eq source · line 1020 · raw

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

def ms_fits source · line 1027 · raw

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

def ms_fv source · line 1040 · raw

@+bit:Bool -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+aok:Bool -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 1051 · 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 1060 · raw

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

def powsim source · line 1071 · raw

@+f:Nat -> @+e:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bok:Bool -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(64n, nb) == bok : Bool} -> @+hb:{fv(bok, v(b), nb) == nb : Nat} -> @+hmb:{mode(md, nb) == True{} : Bool} -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 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(64n, t0) == ct : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.pow_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, e, b, bok, (a, aok)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, Bool.not(ct), of(t0)) : Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def md_init source · line 1088 · 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 1096 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, x, k)

def pow_checked source · line 1105 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Pow.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, x, k)

def pw_val source · line 1110 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 1n+k, k, x, True{}, (0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.One{}), True{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.pow(v(x), k))), of(Nat.pow(v(x), k))) : Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def rlf source · line 1116 · raw

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

def rl_v source · line 1126 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.root_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}

def imid_v source · line 1130 · raw

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

def lt_add_r source · line 1142 · 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 1147 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.inc(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, lo), hi}) == Nat.is_lt(1n, w) : Bool}

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

def srch source · line 1151 · raw

@+f:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+more:Bool -> @+hit:Bool -> @+j:Nat -> @+nlo:Nat -> @+w:Nat -> @+R:Nat -> @+K:Nat -> @+hK:{K == 64n : 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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}

def iroot_big source · line 1194 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+kp:Nat -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.iroot_k(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, n, 2n+kp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.iroot_k(v(n), 2n+kp) : Nat}

def iroot_agrees source · line 1222 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Iroot.agrees(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, n, k)

def nz_of source · line 1233 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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 1236 · 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 1239 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+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.u64_op(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Quot{a, b})) == Nat.div(na, nb) : Nat}

def combsim source · line 1242 · raw

@+f:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+i:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+nn:Nat -> @+ni:Nat -> @+k0:Nat -> @+K:Nat -> @+ok:Bool -> @+more:Bool -> @+cn:Bool -> @+hK:{K == 64n : 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(64n, 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(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, k0)) == cn : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.comb_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, n, i, k, (r, ok), more) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, Bool.not(cn), of(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(nn, k0))) : Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def min_le_a source · line 1285 · 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 1292 · 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 1299 · 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 1303 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+big:Bool -> @+hbig:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{n, k}) == big : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.comb_big(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, n, k, big) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.choose(v(n), v(k))) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>}

def comb_checked source · line 1337 · raw

@+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.Comb.checked(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of, 64n, n, k)