def ms_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1026

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/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

1026def ms_fits(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +md: Bool, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}) -> {C.fits(32n, NF.msn(bit, na, nb)) == ms_ok(bit, a, aok, b, bok) : Bool}:
1027  match bit aok bok:
1028    case False{} _ _:
1029      hA
1030    case True{} True{} True{}:
1031      ok_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb))
1032    case True{} False{} _:
1033      +md1 = unfit_big(na, md, hma, hA)
1034      unfit_mul(na, nb, hA, L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hmb))
1035    case True{} True{} False{}:
1036      +md1 = unfit_big(nb, md, hmb, hB)
1037      unfit_mul_r(na, nb, hB, L.subst(Bool, t => {mode(t, na) == True{} : Bool}, md, True{}, md1, hma))