def sim_rb

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

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

316def sim_rb(+a: WU.U64, +b: WU.U64, +bz: Bool, +hbz: {BN.iz(v(b)) == bz : Bool}, +hfit: {C.fits(64n, BN.nrb(v(a), v(b), bz)) == True{} : Bool}) -> {v(G.gcd_rb(~WU.U64, ~I.u64_op, ~I.u64_is, a, b, bz)) == BN.nrb(v(a), v(b), bz) : Nat}:
317  match bz:
318    case True{}:
319      {==}
320    case False{}:
321      +x1 = Equal.cong(Nat, Nat, t => BN.nbg_a(v(b), t, I.u64_is(NM.IsZero{b})), v(I.u64_op(NM.Rem{a, b})), Nat.mod(v(a), v(b)), UL.ops_rem(a, b, hbz))
322      +x2 = Equal.cong(Bool, Nat, t => BN.nbg_a(v(b), Nat.mod(v(a), v(b)), t), I.u64_is(NM.IsZero{b}), BN.iz(v(b)), UL.tests_is_zero(b))
323      +E = Equal.trans(Nat, BN.nbg_a(v(b), v(I.u64_op(NM.Rem{a, b})), I.u64_is(NM.IsZero{b})), BN.nbg_a(v(b), Nat.mod(v(a), v(b)), I.u64_is(NM.IsZero{b})), BN.nbg_a(v(b), Nat.mod(v(a), v(b)), BN.iz(v(b))), x1, x2)
324      +hfit2 = Equal.trans(Bool, C.fits(64n, BN.nbg_a(v(b), v(I.u64_op(NM.Rem{a, b})), I.u64_is(NM.IsZero{b}))), C.fits(64n, BN.nbg_a(v(b), Nat.mod(v(a), v(b)), BN.iz(v(b)))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), BN.nbg_a(v(b), v(I.u64_op(NM.Rem{a, b})), I.u64_is(NM.IsZero{b})), BN.nbg_a(v(b), Nat.mod(v(a), v(b)), BN.iz(v(b))), E), hfit)
325      Equal.trans(Nat, v(G.bg_a(~WU.U64, ~I.u64_op, ~I.u64_is, b, I.u64_op(NM.Rem{a, b}), I.u64_is(NM.IsZero{b}))), BN.nbg_a(v(b), v(I.u64_op(NM.Rem{a, b})), I.u64_is(NM.IsZero{b})), BN.nbg_a(v(b), Nat.mod(v(a), v(b)), BN.iz(v(b))), sim_bg_a(b, I.u64_op(NM.Rem{a, b}), I.u64_is(NM.IsZero{b}), hfit2), E)