def mod_qs

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64dmrem.bend:44

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/w64.bend as X
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/nat.bend as N
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/w64dm.bend as DM

44def mod_qs(+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(DM.X96(WU.U64{al, ah}, 0), Nat.mul(1n+DM.v(e), SW.value(WU.U64{bl, bh}))) == True{} : Bool}) -> {Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) == Nat.sub(SW.value(WU.U64{al, ah}), Nat.mul(DM.v(X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e)), SW.value(WU.U64{bl, bh}))) : Nat}:
45  +bp = Nat.sub(SW.value(WU.U64{bl, bh}), 1n)
46  +hB = Equal.sym(Nat, 1n+bp, SW.value(WU.U64{bl, bh}), N.sub_add(SW.value(WU.U64{bl, bh}), 1n, vb_pos(bl, bh, hz)))
47  dp = DM.dm_pair(one, h1, al, ah, bl, bh, e, hz, he, bp, hB)
48  +d2 = DM.pr2({Nat.div(SW.value(WU.U64{al, ah}), 1n+bp) == DM.v(DM.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(DM.v(DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat}, dp)
49  +hm = L.subst(Nat, t => {Nat.mod(SW.value(WU.U64{al, ah}), t) == Nat.sub(SW.value(WU.U64{al, ah}), Nat.mul(DM.v(DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), t)) : Nat}, 1n+bp, SW.value(WU.U64{bl, bh}), Equal.sym(Nat, SW.value(WU.U64{bl, bh}), 1n+bp, hB), d2)
50  L.subst(U32, z => {Nat.mod(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) == Nat.sub(SW.value(WU.U64{al, ah}), Nat.mul(DM.v(z), SW.value(WU.U64{bl, bh}))) : Nat}, DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295), X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e), Equal.sym(U32, X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e), DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295), DM.impl_qs(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e)), hm)