~/bend-docscommunity

proofs/math/typed/u64bgcd.bend checks

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

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 ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ./width.bend as WW
import ./u64laws.bend as UL
import ../natural/proof.bend as NP
import ./bgcdnat.bend as BN
import ./w64div.bend as W64D
import ../u64/u64div.bend as PD
import ./w64mul.bend as W64M
import ./natlight.bend as SR
import ./w64m128.bend as M128
import ./w64add.bend as WA
import ./w64sqrt.bend as W64S
import ../../lib/word.bend as WD
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./u32laws.bend as LW
import ../../lib/u32.bend as U
import ../../../src/math/w64.bend as X

Definitions

def v source · line 34 · raw

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

def fits_mono source · line 39 · raw

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

def ndbl_ge source · line 42 · raw

@k:Nat -> @+y:Nat -> {Nat.is_le(y, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ndbl(k, y)) == True{} : Bool}

def dvd_le source · line 50 · raw

@+g:Nat -> @+np:Nat -> @+k:Nat -> @+e:{1n+np == Nat.mul(k, g) : Nat} -> {Nat.is_le(g, 1n+np) == True{} : Bool}

a divisor of 1 + np is at most 1 + np

def gcd_fits_d source · line 58 · raw

@+x:Nat -> @+np:Nat -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 1n+np) == True{} : Bool} -> @d:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, 1n+np), 1n+np) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, 1n+np)) == True{} : Bool}

def gcd_fits_w source · line 61 · raw

@+x:Nat -> @+np:Nat -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 1n+np) == True{} : Bool} -> @w:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, 1n+np), 1n+np) -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, 1n+np)) == True{} : Bool}

def gcd_fits source · line 65 · raw

@+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y)) == True{} : Bool}

def sim_strip_go source · line 74 · raw

@f:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+o:Bool -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.strip_go(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, (x, o))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip_go(f, v(x), o) : Nat}

def sim_strip source · line 88 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.strip(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip(v(x)) : Nat}

def sim_dbl source · line 93 · raw

@c:Nat -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ndbl(c, v(x))) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.dbl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, c, x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ndbl(c, v(x)) : Nat}

def hv source · line 106 · raw

@+l:U32 -> @+h:U32 -> {U32.to_nat(h) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) : Nat}

def kv16 source · line 111 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 16n)} : U32} -> {U32.to_nat(c) == 65536n : Nat}

2^16 and 2^16 - 1 as words c: their values are the Nat literals, reached over an open unit (a closed U32.to_nat(65536) unfolds in unary)

def kv15 source · line 114 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> {U32.to_nat(c) == 65535n : Nat}

def fh_c source · line 118 · raw

@+l:U32 -> @+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 16n)} : U32} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {U32.is_lt(h, c) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})), 65536n) : Bool}

def fh source · line 121 · raw

@+l:U32 -> @+h:U32 -> {U32.is_lt(h, 65536) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})), 65536n) : Bool}

def fzh source · line 124 · raw

@+l:U32 -> @+h:U32 -> {U32.is_zero(h) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})), 0n) : Bool}

def fl_c source · line 127 · raw

@+l:U32 -> @+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 16n)} : U32} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {U32.is_lt(c, l) == Nat.is_lt(65535n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}))) : Bool}

def fl source · line 131 · raw

@+l:U32 -> @+h:U32 -> {U32.is_lt(65535, l) == Nat.is_lt(65535n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h}))) : Bool}

def smv source · line 135 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Small{a, d}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nsm(v(a), v(d)) : Bool}

the Small test is nsm on the values

def s32 source · line 141 · raw

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

(x 2^16) 2^16 == x 2^32

def n48v source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.n48(a) == v(a) : Nat}

def o48_shl_inv_c source · line 154 · raw

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

def o48_shl_inv source · line 162 · raw

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

def tnfn source · line 166 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {U32.to_nat(U32.from_nat(x)) == x : Nat}

a value below 2^32 survives from_nat / to_nat

def k16s source · line 170 · raw

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

def o48_split source · line 174 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+g:Nat -> {Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(16n, Nat.mod(Nat.div(g, 65536n), 65536n)), Nat.mod(g, 65536n)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.div(Nat.div(g, 65536n), 65536n))) == g : Nat}

g = (2^16 r2 + r1) + 2^32 h: r1, r2 the low 16-bit digits, h = g div 2^32

def o48_lo_lt source · line 186 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r1:Nat -> @+r2:Nat -> @+hr1:{Nat.is_lt(r1, 65536n) == True{} : Bool} -> @+hr2:{Nat.is_lt(r2, 65536n) == True{} : Bool} -> {Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(16n, r2), r1), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool}

two 16-bit digits make a value below 2^32

def o48_hi_lt source · line 200 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+g:Nat -> @+hg:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, g) == True{} : Bool} -> @+L0:Nat -> @+h:Nat -> @+es:{Nat.add(L0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, h)) == g : Nat} -> {Nat.is_lt(h, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool}

the high word of g < 2^64 is below 2^32

def of48v source · line 208 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+g:Nat -> @+hg:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, g) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.of48(g)) == g : Nat}

the two words of g < 2^64

def gsv source · line 226 · raw

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

GcdSmall is the gcd

def nbc source · line 233 · raw

@+g:Nat -> @+x:Nat -> @+y:Nat -> @+y2:Nat -> @+z:Bool -> @+z2:Bool -> @+w:Bool -> @+w2:Bool -> @+ey:{y == y2 : Nat} -> @+ez:{z == z2 : Bool} -> @+ew:{w == w2 : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(g, x, y, z, w) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(g, x, y2, z2, w2) : Nat}

nbloop with its arguments rewritten

def sim_bnx source · line 236 · raw

@+g:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @ih:(@+a2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bloop(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, g, (a2, d2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{d2}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Small{a2, d2})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(g, v(a2), v(d2), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{d2}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Small{a2, d2})) : Nat}) -> @+lb:Bool -> @+hl:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Lt{s, a}) == lb : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bloop(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, g, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bnx2(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, s, lb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(g, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nba(v(a), v(s), lb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbd(v(a), v(s), lb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.iz(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbd(v(a), v(s), lb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nsm(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nba(v(a), v(s), lb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbd(v(a), v(s), lb))) : Nat}

def sim_bloop source · line 252 · raw

@f:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+dz:Bool -> @+sm:Bool -> @+hsm:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Small{a, d}) == sm : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bloop(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, (a, d, dz, sm))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(f, v(a), v(d), dz, sm) : Nat}

def sim_exit source · line 268 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Nat -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ndbl(c, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(140n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip(v(a)), v(b), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.iz(v(b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nsm(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip(v(a)), v(b))))) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.dbl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, c, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bloop(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 140n, (0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.strip(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a), b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.IsZero{b}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Small{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.strip(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a), b}))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ndbl(c, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbloop(140n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip(v(a)), v(b), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.iz(v(b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nsm(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nstrip(v(a)), v(b)))) : Nat}

def sim_tw source · line 278 · raw

@f:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:Nat -> @+both:Bool -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ntw(f, v(a), v(b), c, both)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.tw(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, f, a, b, c, both)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.ntw(f, v(a), v(b), c, both) : Nat}

def sim_bg_b source · line 297 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bz:Bool -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbg_b(v(a), v(b), bz)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bg_b(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b, bz)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbg_b(v(a), v(b), bz) : Nat}

def sim_bg_a source · line 307 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+az:Bool -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbg_a(v(a), v(b), az)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.bg_a(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b, az)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbg_a(v(a), v(b), az) : Nat}

def sim_rb source · line 316 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bz:Bool -> @+hbz:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.iz(v(b)) == bz : Bool} -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nrb(v(a), v(b), bz)) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd_rb(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b, bz)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nrb(v(a), v(b), bz) : Nat}

def sim_bin source · line 327 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hfit:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbin(v(a), v(b))) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.gcd_bin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/bgcdnat.nbin(v(a), v(b)) : Nat}

def gcd_val source · line 334 · 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}