def bl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:429

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

429# the loop from (a odd, 2k) with a * 2k < 2^f and f <= 140 computes gcd(a, 2k)
430def bl(f: Nat, +a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +k: Nat, +hb: {Nat.is_lt(Nat.mul(a, Nat.double(k)), C.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))) == M.gcd(a, Nat.double(k)) : Nat}:
431  match f k:
432    case f0 0n:
433      bl_zero(f0, a)
434    case 0n 1n+kp:
435      Empty.absurd({nbloop(0n, a, Nat.double(1n+kp), iz(Nat.double(1n+kp)), nsm(a, Nat.double(1n+kp))) == M.gcd(a, Nat.double(1n+kp)) : Nat}, pos_absurd1(Nat.mul(a, Nat.double(1n+kp)), mul_pos(a, odd_pos(a, ha), Nat.double(1n+kp), {==}), hb))
436    case 1n+ +g 1n+ +kp:
437      +hg = N.le_trans(g, 1n+g, 140n, N.le_succ(g), hf)
438      bl_sm(g, a, kp, nsm(a, Nat.double(1n+kp)), bl_step(g, a, ha, kp, half_bound(a, kp, g, hb), hf, a2 => ha2 => k2 => hb2 => bl(g, a2, ha2, k2, hb2, hg), Nat.is_lt(nstrip(Nat.double(1n+kp)), a), {==}))