def qs_pair

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

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/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/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

166# the down loop from an estimate q with x < (q + 1) b: q' b <= x < (q' + 1) b
167def qs_pair(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}, +hX: {Nat.is_lt(X96(xl, xh), Nat.mul(C.shift(32n, one), SW.value(b))) == True{} : Bool}, +hu: {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), SW.value(b))) == True{} : Bool}) -> {Nat.is_le(QB(b, QS(xl, xh, b, q, m)), X96(xl, xh)) == True{} : Bool} & {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(QS(xl, xh, b, q, m)), SW.value(b))) == True{} : Bool}:
168  (qdn(Nat.add(v(q), 1n), one, h1, xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)), v(q), L.subst(Nat, z => {Nat.is_lt(v(q), z) == True{} : Bool}, 1n+v(q), Nat.add(v(q), 1n), Equal.sym(Nat, Nat.add(v(q), 1n), 1n+v(q), WA.plus1(v(q))), N.lt_succ(v(q))), {==}, {==}), qup2(Nat.add(v(q), 1n), one, h1, xl, xh, b, q, X.over96(xl, xh, X.mul_32_64(q, b)), v(q), L.subst(Nat, z => {Nat.is_lt(v(q), z) == True{} : Bool}, 1n+v(q), Nat.add(v(q), 1n), Equal.sym(Nat, Nat.add(v(q), 1n), 1n+v(q), WA.plus1(v(q))), N.lt_succ(v(q))), {==}, {==}, hu))