def ms_fv

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

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

1040def ms_fv(+bit: Bool, +a: WU.U64, +aok: Bool, +b: WU.U64, +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}:
1041  match bit aok bok:
1042    case False{} _ _:
1043      ha
1044    case True{} True{} True{}:
1045      fv_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb), C.fits(64n, Nat.mul(na, nb)), {==})
1046    case True{} False{} _:
1047      {==}
1048    case True{} True{} False{}:
1049      {==}