def bfirst

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

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT

480# a odd, b > 0, a b < 2^139: the loop computes gcd(a, b)
481def bfirst(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +bp: Nat, +hab: {Nat.is_lt(Nat.mul(a, 1n+bp), C.pow2(139n)) == True{} : Bool}) -> {nbloop(140n, a, 1n+bp, iz(1n+bp), nsm(a, 1n+bp)) == M.gcd(a, 1n+bp) : Nat}:
482  +k1 = N.le_trans(1n+bp, Nat.mul(1n+bp, a), Nat.mul(a, 1n+bp), RT.le_mul_pos(1n+bp, a, odd_pos(a, ha)), N.eq_le(Nat.mul(1n+bp, a), Nat.mul(a, 1n+bp), NA.mul_comm(1n+bp, a)))
483  +k2 = N.lt_le_trans(1n+bp, C.pow2(139n), C.pow2(140n), N.le_lt_trans(1n+bp, Nat.mul(a, 1n+bp), C.pow2(139n), k1, hab), N.pow2_mono(139n, 140n, {==}))
484  +hs = odd_eq(nstrip(1n+bp), strip_odd(140n, 1n+bp, {==}, k2, odd(1n+bp), {==}))
485  +hga = Equal.sym(Nat, M.gcd(a, nstrip(1n+bp)), M.gcd(a, 1n+bp), strip_gcd(a, ha, 140n, 1n+bp, odd(1n+bp), {==}))
486  +hsa = NF.mul_le_r(a, nstrip(1n+bp), 1n+bp, strip_le(140n, 1n+bp, odd(1n+bp)))
487  bf_sm(a, bp, nsm(a, 1n+bp), bf_case(a, ha, bp, hab, hs, hga, hsa, Nat.is_lt(nstrip(1n+bp), a), {==}))