def dm_pair

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64dm.bend:208

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
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/lib/logic.bend as L

208# the big-divisor quotient: q b <= a < (q + 1) b
209def dm_pair(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +e: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +he: {Nat.is_lt(X96(WU.U64{al, ah}, 0), Nat.mul(1n+v(e), SW.value(WU.U64{bl, bh}))) == True{} : Bool}, +bp: Nat, +hB: {SW.value(WU.U64{bl, bh}) == 1n+bp : Nat}) -> {Nat.div(SW.value(WU.U64{al, ah}), 1n+bp) == v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)) : Nat} & {Nat.mod(SW.value(WU.U64{al, ah}), 1n+bp) == Nat.sub(SW.value(WU.U64{al, ah}), Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat}:
210  +vbv = SW.value(WU.U64{bl, bh})
211  +hX = dm_hx(one, h1, al, ah, bl, bh, hz)
212  pr = qs_pair(one, h1, WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295, {==}, hX, he)
213  dv = qs_fin2(X96(WU.U64{al, ah}, 0), v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), vbv, bp, hB, pr)
214  L.subst(Nat, z => {Nat.div(z, 1n+bp) == v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)) : Nat} & {Nat.mod(z, 1n+bp) == Nat.sub(z, Nat.mul(v(QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat}, X96(WU.U64{al, ah}, 0), SW.value(WU.U64{al, ah}), x96_0(WU.U64{al, ah}), dv)