def cm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:212

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/spec/math/generic.bend as SG
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/proofs/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

212def cm(+q: WU.U64, +b: WU.U64, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(64n, n) == c : Bool}) -> {G.ok(WU.U64, G.cmul(~WU.U64, ~I.u64_op, ~I.u64_is, q, b)) == SG.checked(~WU.U64, ~SG.u64_of, 64n, n) : Result<&2, &2, NM.NumError, WU.U64>}:
213  match c:
214    case True{}:
215      +hmo2 = mo_of(q, b, n, hn, True{}, hc)
216      %Equal.sym(Bool, I.u64_is(NM.MulOver{q, b}), False{}, hmo2) : {G.ok(WU.U64, G.fits(WU.U64, _, I.u64_op(NM.Mul{q, b}))) == SG.checked(~WU.U64, ~SG.u64_of, 64n, n) : Result<&2, &2, NM.NumError, WU.U64>}
217      %Equal.sym(Bool, C.fits(64n, n), True{}, hc) : {Done{I.u64_op(NM.Mul{q, b})} == SG.checked_pick(~WU.U64, ~SG.u64_of, n, _) : Result<&2, &2, NM.NumError, WU.U64>}
218      %Equal.sym(WU.U64, I.u64_op(NM.Mul{q, b}), of(n), as_of(I.u64_op(NM.Mul{q, b}), n, Equal.trans(Nat, v(I.u64_op(NM.Mul{q, b})), Nat.mul(v(q), v(b)), n, LW.ops_mul(q, b, hmo2), hn))) : {Done{_} == Done{of(n)} : Result<&2, &2, NM.NumError, WU.U64>}
219      {==}
220    case False{}:
221      +hmo = mo_of(q, b, n, hn, False{}, hc)
222      %Equal.sym(Bool, I.u64_is(NM.MulOver{q, b}), True{}, hmo) : {G.ok(WU.U64, G.fits(WU.U64, _, I.u64_op(NM.Mul{q, b}))) == SG.checked(~WU.U64, ~SG.u64_of, 64n, n) : Result<&2, &2, NM.NumError, WU.U64>}
223      %Equal.sym(Bool, C.fits(64n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~WU.U64, ~SG.u64_of, n, _) : Result<&2, &2, NM.NumError, WU.U64>}
224      {==}