def gcd_val

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:334

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/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as UL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN

334def gcd_val(+K: Nat, +hK: {K == 64n : Nat}, +a: WU.U64, +b: WU.U64) -> {v(G.gcd(~WU.U64, ~I.u64_op, ~I.u64_is, a, b)) == M.gcd(v(a), v(b)) : Nat}:
335  +hw = Equal.trans(Bool, Nat.is_le(Nat.add(K, K), 139n), Nat.is_le(Nat.add(64n, 64n), 139n), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(Nat.add(t, t), 139n), K, 64n, hK), {==})
336  +hw140 = Equal.trans(Bool, Nat.is_le(K, 140n), Nat.is_le(64n, 140n), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(t, 140n), K, 64n, hK), {==})
337  +nb = BN.nbin_gcd(K, hw, hw140, v(a), v(b), UL.val_lt(K, hK, b))
338  +hfit = Equal.trans(Bool, C.fits(64n, BN.nbin(v(a), v(b))), C.fits(64n, M.gcd(v(a), v(b))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), BN.nbin(v(a), v(b)), M.gcd(v(a), v(b)), nb), gcd_fits(v(a), v(b), UL.vb(a), UL.vb(b)))
339  Equal.trans(Nat, v(G.gcd_bin(~WU.U64, ~I.u64_op, ~I.u64_is, a, b)), BN.nbin(v(a), v(b)), M.gcd(v(a), v(b)), sim_bin(a, b, hfit), nb)