def ms_fv

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

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/math/typed/natfuel.bend as NF

1039def ms_fv(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +ha: {fv(aok, v(a), na) == na : Nat}, +hb: {fv(bok, v(b), nb) == nb : Nat}) -> {fv(ms_ok(bit, a, aok, b, bok), v(ms_a(bit, a, b)), NF.msn(bit, na, nb)) == NF.msn(bit, na, nb) : Nat}:
1040  match bit aok bok:
1041    case False{} _ _:
1042      ha
1043    case True{} True{} True{}:
1044      fv_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb), C.fits(32n, Nat.mul(na, nb)), {==})
1045    case True{} False{} _:
1046      {==}
1047    case True{} True{} False{}:
1048      {==}