def sim_bin

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

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/num.bend as NM
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

327def sim_bin(+a: WU.U64, +b: WU.U64, +hfit: {C.fits(64n, BN.nbin(v(a), v(b))) == True{} : Bool}) -> {v(G.gcd_bin(~WU.U64, ~I.u64_op, ~I.u64_is, a, b)) == BN.nbin(v(a), v(b)) : Nat}:
328  +x = Equal.cong(Bool, Nat, t => BN.nrb(v(a), v(b), t), I.u64_is(NM.IsZero{b}), BN.iz(v(b)), UL.tests_is_zero(b))
329  +hfit2 = Equal.trans(Bool, C.fits(64n, BN.nrb(v(a), v(b), I.u64_is(NM.IsZero{b}))), C.fits(64n, BN.nbin(v(a), v(b))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), BN.nrb(v(a), v(b), I.u64_is(NM.IsZero{b})), BN.nbin(v(a), v(b)), x), hfit)
330  Equal.trans(Nat, v(G.gcd_rb(~WU.U64, ~I.u64_op, ~I.u64_is, a, b, I.u64_is(NM.IsZero{b}))), BN.nrb(v(a), v(b), I.u64_is(NM.IsZero{b})), BN.nbin(v(a), v(b)), sim_rb(a, b, I.u64_is(NM.IsZero{b}), Equal.sym(Bool, I.u64_is(NM.IsZero{b}), BN.iz(v(b)), UL.tests_is_zero(b)), hfit2), x)