~/bend-docscommunity

proofs/math/typed/bgcdnat.bend checks

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

19 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/natural.bend as S
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/proof.bend as NP
import ../natural/lcm.bend as LC
import ../natural/gcd.bend as GD
import ../natural/arith.bend as NR
import ../natural/bits.bend as BT
import ./natfuel.bend as NF
import ../../lib/u32half.bend as UH
import ../natural/roots.bend as RT
import ../../lib/two_list.bend as TL
import ../natural/fact.bend as FA
import ../../lib/arith.bend as AR
import ../natural/misc.bend as MS

Definitions

def dvd2 source · line 31 · raw

@+d:Nat -> @+u:Nat -> @+v:Nat -> Type

def Transfer source · line 35 · raw

@+x:Nat -> @+y:Nat -> @+u:Nat -> @+v:Nat -> Type

every common divisor of (x, y), given by its quotients, divides u and v

def into3 source · line 38 · raw

@+g:Nat -> @+u:Nat -> @+v:Nat -> @du:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(g, u) -> @dv:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(g, v) -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(g, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v))

def into2 source · line 43 · raw

@+g:Nat -> @+u:Nat -> @+v:Nat -> @p:dvd2(g, u, v) -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(g, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v))

def into1 source · line 47 · raw

@+x:Nat -> @+y:Nat -> @+u:Nat -> @+v:Nat -> @t:Transfer(x, y, u, v) -> @dl:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y), x) -> @dr:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y), y) -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v))

def into source · line 52 · raw

@+x:Nat -> @+y:Nat -> @+u:Nat -> @+v:Nat -> @t:Transfer(x, y, u, v) -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v))

def gcd_eq2 source · line 55 · raw

@+x:Nat -> @+y:Nat -> @+u:Nat -> @+v:Nat -> @a:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v)) -> @b:0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y)) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v) : Nat}

def gcd_eq source · line 60 · raw

@+x:Nat -> @+y:Nat -> @+u:Nat -> @+v:Nat -> @t1:Transfer(x, y, u, v) -> @t2:Transfer(u, v, x, y) -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(x, y) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(u, v) : Nat}

def swap_t source · line 63 · raw

@+x:Nat -> @+y:Nat -> Transfer(x, y, y, x)

def gcd_comm source · line 66 · raw

@+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(b, a) : Nat}

def sub_t1_at source · line 71 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+kx:Nat -> @+ky:Nat -> @+ex:{a == Nat.mul(kx, d) : Nat} -> @+ey:{b == Nat.mul(ky, d) : Nat} -> dvd2(d, a, Nat.sub(b, a))

def sub_t2_at source · line 77 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> @+d:Nat -> @+kx:Nat -> @+kz:Nat -> @+ex:{a == Nat.mul(kx, d) : Nat} -> @+ez:{Nat.sub(b, a) == Nat.mul(kz, d) : Nat} -> dvd2(d, a, b)

def gcd_sub source · line 81 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.sub(b, a)) : Nat}

def rec_t2_at source · line 86 · raw

@+a:Nat -> @+bp:Nat -> @+d:Nat -> @+kn:Nat -> @+kr:Nat -> @+en:{1n+bp == Nat.mul(kn, d) : Nat} -> @+er:{Nat.mod(a, 1n+bp) == Nat.mul(kr, d) : Nat} -> dvd2(d, a, 1n+bp)

def gcd_rec source · line 89 · raw

@+a:Nat -> @+bp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(1n+bp, Nat.mod(a, 1n+bp)) : Nat}

def odd source · line 94 · raw

@+n:Nat -> Bool

def dmul source · line 98 · raw

@+q:Nat -> @+d:Nat -> {Nat.mul(Nat.double(q), d) == Nat.double(Nat.mul(q, d)) : Nat}

2q * d = 2 (q d)

def even_form source · line 102 · raw

@+n:Nat -> @+h:{Nat.mod(n, 2n) == 0n : Nat} -> {n == Nat.double(Nat.div(n, 2n)) : Nat}

def odd_form source · line 106 · raw

@+n:Nat -> @+h:{Nat.mod(n, 2n) == 1n : Nat} -> {n == 1n+Nat.double(Nat.div(n, 2n)) : Nat}

def odd_eq source · line 110 · raw

@+n:Nat -> @+h:{odd(n) == True{} : Bool} -> {Nat.mod(n, 2n) == 1n : Nat}

def mod2_big source · line 114 · raw

@+n:Nat -> @+x:Nat -> @+hr:{Nat.mod(n, 2n) == 2n+x : Nat} -> Empty

n mod 2 is 0 or 1

def odd_dvd_r source · line 119 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+d:Nat -> @+ka:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+r:Nat -> @+hr:{Nat.mod(d, 2n) == r : Nat} -> {Nat.mod(d, 2n) == 1n : Nat}

a divisor of an odd number is odd

def odd2_m source · line 133 · raw

@+m:Nat -> @+d:Nat -> @+hd:{Nat.mod(d, 2n) == 1n : Nat} -> @+kb:Nat -> @+eb:{Nat.double(m) == Nat.mul(kb, d) : Nat} -> @+r:Nat -> @+hr:{Nat.mod(kb, 2n) == r : Nat} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.dvd(d, m)

an odd d dividing 2 m divides m

def odd2_t1_at source · line 154 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+m:Nat -> @+d:Nat -> @+ka:Nat -> @+kb:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+eb:{Nat.double(m) == Nat.mul(kb, d) : Nat} -> dvd2(d, a, m)

def odd2_t2_at source · line 157 · raw

@+a:Nat -> @+m:Nat -> @+d:Nat -> @+ka:Nat -> @+km:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+em:{m == Nat.mul(km, d) : Nat} -> dvd2(d, a, Nat.double(m))

def gcd_odd2 source · line 161 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, m) : Nat}

a odd: gcd(a, 2 m) = gcd(a, m)

def iz source · line 170 · raw

@+n:Nat -> Bool

def nstrip_go source · line 173 · raw

@fuel:Nat -> @+x:Nat -> @o:Bool -> Nat

def nstrip source · line 182 · raw

@+x:Nat -> Nat

def nba source · line 185 · raw

@+a:Nat -> @+s:Nat -> @less:Bool -> Nat

def nbd source · line 192 · raw

@+a:Nat -> @+s:Nat -> @less:Bool -> Nat

def nsm source · line 203 · raw

@+a:Nat -> @+d:Nat -> Bool

the U64 loop's Small test on the values (both below 2^48, a at least 2^16): the loop then returns gcd(a, d) at once. The bounds are Nat literals: U32.to_nat(65536) would unfold into 2^16 successors whenever a conversion compares it.

def nbloop source · line 206 · raw

@fuel:Nat -> @+a:Nat -> @+d:Nat -> @dz:Bool -> @sm:Bool -> Nat

def ndbl source · line 217 · raw

@c:Nat -> @+x:Nat -> Nat

def nev2 source · line 224 · raw

@+a:Nat -> @+b:Nat -> Bool

def ntw source · line 227 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @both:Bool -> Nat

def nbg_b source · line 236 · raw

@+a:Nat -> @+b:Nat -> @bz:Bool -> Nat

def nbg_a source · line 243 · raw

@+a:Nat -> @+b:Nat -> @az:Bool -> Nat

def nrb source · line 250 · raw

@+a:Nat -> @+b:Nat -> @bz:Bool -> Nat

def nbin source · line 257 · raw

@+a:Nat -> @+b:Nat -> Nat

def not_odd_r source · line 263 · raw

@+n:Nat -> @+h:{odd(n) == False{} : Bool} -> @+r:Nat -> @+hr:{Nat.mod(n, 2n) == r : Nat} -> {Nat.mod(n, 2n) == 0n : Nat}

not odd is even

def not_odd source · line 273 · raw

@+n:Nat -> @+h:{odd(n) == False{} : Bool} -> {Nat.mod(n, 2n) == 0n : Nat}

def strip_gcd source · line 277 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @f:Nat -> @+x:Nat -> @+o:Bool -> @+ho:{odd(x) == o : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, nstrip_go(f, x, o)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, x) : Nat}

a odd: gcd(a, strip(x)) = gcd(a, x), whatever the fuel

def pos_absurd1 source · line 289 · raw

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

def dlt_inv_b source · line 292 · raw

@+u:Nat -> @+v:Nat -> @+e:{Nat.is_lt(Nat.double(u), Nat.double(v)) == True{} : Bool} -> @+bv:Bool -> @+hb:{Nat.is_lt(u, v) == bv : Bool} -> {Nat.is_lt(u, v) == True{} : Bool}

def double_lt_inv source · line 301 · raw

@+u:Nat -> @+v:Nat -> @+e:{Nat.is_lt(Nat.double(u), Nat.double(v)) == True{} : Bool} -> {Nat.is_lt(u, v) == True{} : Bool}

2u < 2v gives u < v

def div2_le source · line 304 · raw

@+x:Nat -> {Nat.is_le(Nat.div(x, 2n), x) == True{} : Bool}

def half_pos source · line 312 · raw

@+x:Nat -> @+hx:{Nat.is_lt(0n, x) == True{} : Bool} -> @+ev:{x == Nat.double(Nat.div(x, 2n)) : Nat} -> @+h:Nat -> @+hh:{Nat.div(x, 2n) == h : Nat} -> {Nat.is_lt(0n, Nat.div(x, 2n)) == True{} : Bool}

an even positive x = 2 (x / 2) has x / 2 > 0

def strip_odd source · line 322 · raw

@f:Nat -> @+x:Nat -> @+hx:{Nat.is_lt(0n, x) == True{} : Bool} -> @+hb:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(f)) == True{} : Bool} -> @+o:Bool -> @+ho:{odd(x) == o : Bool} -> {odd(nstrip_go(f, x, o)) == True{} : Bool}

with fuel f and x < 2^f, stripping reaches an odd number

def strip_le source · line 334 · raw

@f:Nat -> @+x:Nat -> @+o:Bool -> {Nat.is_le(nstrip_go(f, x, o), x) == True{} : Bool}

stripping never grows

def mod2_double source · line 345 · raw

@+k:Nat -> {Nat.mod(Nat.double(k), 2n) == 0n : Nat}

def odd_true source · line 351 · raw

@+n:Nat -> @+h:{Nat.mod(n, 2n) == 1n : Nat} -> {odd(n) == True{} : Bool}

def odd_pos source · line 354 · raw

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

def double_sub source · line 358 · raw

@+p:Nat -> @+q:Nat -> {Nat.sub(Nat.double(p), Nat.double(q)) == Nat.double(Nat.sub(p, q)) : Nat}

def odd_sub source · line 363 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+s:Nat -> @+hs:{Nat.mod(s, 2n) == 1n : Nat} -> {Nat.sub(a, s) == Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(s, 2n))) : Nat}

odd a - odd s is even

def mul_pos source · line 368 · raw

@+a:Nat -> @+ha:{Nat.is_lt(0n, a) == True{} : Bool} -> @+d:Nat -> @+hd:{Nat.is_lt(0n, d) == True{} : Bool} -> {Nat.is_lt(0n, Nat.mul(a, d)) == True{} : Bool}

def bl_zero source · line 372 · raw

@f:Nat -> @+a:Nat -> {nbloop(f, a, 0n, True{}, nsm(a, 0n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 0n) : Nat}

def half_bound source · line 380 · raw

@+a:Nat -> @+kp:Nat -> @+g:Nat -> @+hb:{Nat.is_lt(Nat.mul(a, Nat.double(1n+kp)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(1n+g)) == True{} : Bool} -> {Nat.is_lt(Nat.mul(a, 1n+kp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool}

a (1 + kp) < 2^g from a (2 + 2 kp) < 2^(1 + g)

def strip_even source · line 385 · raw

@+kp:Nat -> {Nat.is_le(nstrip(Nat.double(1n+kp)), 1n+kp) == True{} : Bool}

strip(2 (1 + kp)) <= 1 + kp

def bl_case source · line 391 · raw

@+g:Nat -> @+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+kp:Nat -> @+hbg:{Nat.is_lt(Nat.mul(a, 1n+kp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool} -> @ih:(@+a2:Nat -> @+ha2:{Nat.mod(a2, 2n) == 1n : Nat} -> @+k2:Nat -> @+hb2:{Nat.is_lt(Nat.mul(a2, Nat.double(k2)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool} -> {nbloop(g, a2, Nat.double(k2), iz(Nat.double(k2)), nsm(a2, Nat.double(k2))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a2, Nat.double(k2)) : Nat}) -> @+hs:{Nat.mod(nstrip(Nat.double(1n+kp)), 2n) == 1n : Nat} -> @+hsle:{Nat.is_le(nstrip(Nat.double(1n+kp)), 1n+kp) == True{} : Bool} -> @+hga:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(1n+kp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, nstrip(Nat.double(1n+kp))) : Nat} -> @+hsa:{Nat.is_le(Nat.mul(a, nstrip(Nat.double(1n+kp))), Nat.mul(a, 1n+kp)) == True{} : Bool} -> @+lb:Bool -> @+hl:{Nat.is_lt(nstrip(Nat.double(1n+kp)), a) == lb : Bool} -> {nbloop(g, nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb), iz(nbd(a, nstrip(Nat.double(1n+kp)), lb)), nsm(nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(1n+kp)) : Nat}

def bl_step source · line 411 · raw

@+g:Nat -> @+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+kp:Nat -> @+hbg:{Nat.is_lt(Nat.mul(a, 1n+kp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool} -> @+hf1:{Nat.is_le(1n+g, 140n) == True{} : Bool} -> @ih:(@+a2:Nat -> @+ha2:{Nat.mod(a2, 2n) == 1n : Nat} -> @+k2:Nat -> @+hb2:{Nat.is_lt(Nat.mul(a2, Nat.double(k2)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool} -> {nbloop(g, a2, Nat.double(k2), iz(Nat.double(k2)), nsm(a2, Nat.double(k2))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a2, Nat.double(k2)) : Nat}) -> @+lb:Bool -> @+hl:{Nat.is_lt(nstrip(Nat.double(1n+kp)), a) == lb : Bool} -> {nbloop(g, nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb), iz(nbd(a, nstrip(Nat.double(1n+kp)), lb)), nsm(nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(1n+kp)) : Nat}

one step of the loop, from the induction hypothesis for fuel g

def bl_sm source · line 422 · raw

@+g:Nat -> @+a:Nat -> @+kp:Nat -> @sm:Bool -> @+hn:{nbloop(g, nba(a, nstrip(Nat.double(1n+kp)), Nat.is_lt(nstrip(Nat.double(1n+kp)), a)), nbd(a, nstrip(Nat.double(1n+kp)), Nat.is_lt(nstrip(Nat.double(1n+kp)), a)), iz(nbd(a, nstrip(Nat.double(1n+kp)), Nat.is_lt(nstrip(Nat.double(1n+kp)), a))), nsm(nba(a, nstrip(Nat.double(1n+kp)), Nat.is_lt(nstrip(Nat.double(1n+kp)), a)), nbd(a, nstrip(Nat.double(1n+kp)), Nat.is_lt(nstrip(Nat.double(1n+kp)), a)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(1n+kp)) : Nat} -> {nbloop(1n+g, a, Nat.double(1n+kp), iz(Nat.double(1n+kp)), sm) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(1n+kp)) : Nat}

a small pair ends the loop with its gcd; otherwise it steps

def bl source · line 430 · raw

@f:Nat -> @+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+k:Nat -> @+hb:{Nat.is_lt(Nat.mul(a, Nat.double(k)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(f)) == True{} : Bool} -> @+hf:{Nat.is_le(f, 140n) == True{} : Bool} -> {nbloop(f, a, Nat.double(k), iz(Nat.double(k)), nsm(a, Nat.double(k))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, Nat.double(k)) : Nat}

the loop from (a odd, 2k) with a * 2k < 2^f and f <= 140 computes gcd(a, 2k)

def mul_lt_sq source · line 440 · raw

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

def bf_case source · line 454 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+bp:Nat -> @+hab:{Nat.is_lt(Nat.mul(a, 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> @+hs:{Nat.mod(nstrip(1n+bp), 2n) == 1n : Nat} -> @+hga:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, nstrip(1n+bp)) : Nat} -> @+hsa:{Nat.is_le(Nat.mul(a, nstrip(1n+bp)), Nat.mul(a, 1n+bp)) == True{} : Bool} -> @+lb:Bool -> @+hl:{Nat.is_lt(nstrip(1n+bp), a) == lb : Bool} -> {nbloop(139n, nba(a, nstrip(1n+bp), lb), nbd(a, nstrip(1n+bp), lb), iz(nbd(a, nstrip(1n+bp), lb)), nsm(nba(a, nstrip(1n+bp), lb), nbd(a, nstrip(1n+bp), lb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) : Nat}

def bf_sm source · line 473 · raw

@+a:Nat -> @+bp:Nat -> @sm:Bool -> @+hn:{nbloop(139n, nba(a, nstrip(1n+bp), Nat.is_lt(nstrip(1n+bp), a)), nbd(a, nstrip(1n+bp), Nat.is_lt(nstrip(1n+bp), a)), iz(nbd(a, nstrip(1n+bp), Nat.is_lt(nstrip(1n+bp), a))), nsm(nba(a, nstrip(1n+bp), Nat.is_lt(nstrip(1n+bp), a)), nbd(a, nstrip(1n+bp), Nat.is_lt(nstrip(1n+bp), a)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) : Nat} -> {nbloop(140n, a, 1n+bp, iz(1n+bp), sm) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) : Nat}

def bfirst source · line 481 · raw

@+a:Nat -> @+ha:{Nat.mod(a, 2n) == 1n : Nat} -> @+bp:Nat -> @+hab:{Nat.is_lt(Nat.mul(a, 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> {nbloop(140n, a, 1n+bp, iz(1n+bp), nsm(a, 1n+bp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) : Nat}

a odd, b > 0, a b < 2^139: the loop computes gcd(a, b)

def ev_ta source · line 491 · raw

@+oa:Bool -> @+ob:Bool -> @+h:{Bool.not(Bool.or(oa, ob)) == True{} : Bool} -> {oa == False{} : Bool}

def ev_tb source · line 498 · raw

@+oa:Bool -> @+ob:Bool -> @+h:{Bool.not(Bool.or(oa, ob)) == True{} : Bool} -> {ob == False{} : Bool}

def ev_fb source · line 507 · raw

@+oa:Bool -> @+ob:Bool -> @+h:{Bool.not(Bool.or(oa, ob)) == False{} : Bool} -> @+hoa:{oa == False{} : Bool} -> {ob == True{} : Bool}

def add_self source · line 516 · raw

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

def gcd_twice source · line 520 · raw

@+a:Nat -> @+b:Nat -> @+ea:{a == Nat.double(Nat.div(a, 2n)) : Nat} -> @+eb:{b == Nat.double(Nat.div(b, 2n)) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(Nat.div(a, 2n), Nat.div(b, 2n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(Nat.div(a, 2n), Nat.div(b, 2n))) : Nat}

gcd(2a, 2b) = gcd(a, b) + gcd(a, b)

def exit_gcd source · line 526 · raw

@+a:Nat -> @+b:Nat -> @+oa:Bool -> @+hoa:{odd(a) == oa : Bool} -> @+hev:{Bool.not(Bool.or(odd(a), odd(b))) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(nstrip(a), b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) : Nat}

the exit: gcd(strip a, b) = gcd(a, b) when a or b is odd

def tw_exit source · line 534 · raw

@+a:Nat -> @+b:Nat -> @+ha0:{Nat.is_lt(0n, a) == True{} : Bool} -> @+ha140:{Nat.is_lt(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(140n)) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> @+hev:{nev2(a, b) == False{} : Bool} -> @+hb0:{Nat.is_lt(0n, b) == True{} : Bool} -> @+bv:Nat -> @+hbv:{b == bv : Nat} -> {nbloop(140n, nstrip(a), b, iz(b), nsm(nstrip(a), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) : Nat}

def tw_case source · line 545 · raw

@+g:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha0:{Nat.is_lt(0n, a) == True{} : Bool} -> @+hb0:{Nat.is_lt(0n, b) == True{} : Bool} -> @+haf:{Nat.is_lt(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(1n+g)) == True{} : Bool} -> @+hf:{Nat.is_le(1n+g, 140n) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> @ih:(@+a2:Nat -> @+b2:Nat -> @+c2:Nat -> @+ha2:{Nat.is_lt(0n, a2) == True{} : Bool} -> @+hb2:{Nat.is_lt(0n, b2) == True{} : Bool} -> @+haf2:{Nat.is_lt(a2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(g)) == True{} : Bool} -> @+hab2:{Nat.is_lt(Nat.mul(a2, b2), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> {ntw(g, a2, b2, c2, nev2(a2, b2)) == ndbl(c2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a2, b2)) : Nat}) -> @+ev:Bool -> @+hev:{nev2(a, b) == ev : Bool} -> {ntw(1n+g, a, b, c, ev) == ndbl(c, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b)) : Nat}

def tw source · line 561 · raw

@f:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha0:{Nat.is_lt(0n, a) == True{} : Bool} -> @+hb0:{Nat.is_lt(0n, b) == True{} : Bool} -> @+haf:{Nat.is_lt(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(f)) == True{} : Bool} -> @+hf:{Nat.is_le(f, 140n) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(139n)) == True{} : Bool} -> {ntw(f, a, b, c, nev2(a, b)) == ndbl(c, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b)) : Nat}

halving while both are even: ntw computes 2^c gcd(a, b) (as c doublings)

def top_r source · line 571 · raw

@+w:Nat -> @+hw:{Nat.is_le(Nat.add(w, w), 139n) == True{} : Bool} -> @+hw140:{Nat.is_le(w, 140n) == True{} : Bool} -> @+a:Nat -> @+bp:Nat -> @+hb:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(w)) == True{} : Bool} -> @+rv:Nat -> @+hr:{Nat.mod(a, 1n+bp) == rv : Nat} -> {nbg_b(1n+bp, Nat.mod(a, 1n+bp), iz(Nat.mod(a, 1n+bp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, 1n+bp) : Nat}

def nbin_gcd source · line 588 · raw

@+w:Nat -> @+hw:{Nat.is_le(Nat.add(w, w), 139n) == True{} : Bool} -> @+hw140:{Nat.is_le(w, 140n) == True{} : Bool} -> @+a:Nat -> @+b:Nat -> @+hb:{Nat.is_lt(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(w)) == True{} : Bool} -> {nbin(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) : Nat}

the binary gcd of a, b < 2^w (w + w <= 139) is gcd(a, b)