def dmq_bg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64dmtop.bend:33

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/math/typed/w64dm.bend as DM

33def dmq_bg(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +e: U32, +hb: {X.is_zero(WU.U64{bl, bh}) == False{} : Bool}, +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}) -> {SW.value(WU.U64{X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e), 0}) == Nat.div(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}:
34  +bp = Nat.sub(SW.value(WU.U64{bl, bh}), 1n)
35  +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)))
36  dp = DM.dm_pair(one, h1, al, ah, bl, bh, e, hz, he, bp, hB)
37  +d1 = DM.pr1({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)
38  +eq = Equal.cong(U32, Nat, t => DM.v(t), 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))
39  Equal.trans(Nat, SW.value(WU.U64{X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e), 0}), DM.v(X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e)), Nat.div(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), DM.u32_0(X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e)), Equal.trans(Nat, DM.v(X.q_start(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e)), DM.v(DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), Nat.div(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), eq, Equal.trans(Nat, DM.v(DM.QS(WU.U64{al, ah}, 0, WU.U64{bl, bh}, e, 4294967295)), Nat.div(SW.value(WU.U64{al, ah}), 1n+bp), Nat.div(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), Equal.sym(Nat, 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)), d1), Equal.cong(Nat, Nat, t => Nat.div(SW.value(WU.U64{al, ah}), t), 1n+bp, SW.value(WU.U64{bl, bh}), Equal.sym(Nat, SW.value(WU.U64{bl, bh}), 1n+bp, hB)))))