def qr_q

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:438

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/f64.bend as SF
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/f64.bend as F
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/w64dmrem.bend as DR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmtop.bend as DQ

438def qr_q(+x: F.F64, +y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {Nat.mod(SW.value(X.pfst(F.fm_qr(x, y))), 2n) == Nat.mod(Nat.div(C.shift(DD(x, y), SW.value(F.dmant(x))), SW.value(F.dmant(y))), 2n) : Nat}:
439  +xw = F.dmant(x)
440  +yw = F.dmant(y)
441  +D = DD(x, y)
442  +bp = bpv(y)
443  +V = SW.value(yw)
444  +e0 = Equal.cong(WU.U64 & WU.U64, Nat, u => Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, u))), 2n), X.divmod(xw, yw), (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw))), eta(X.divmod(xw, yw)))
445  +hr0 = Equal.trans(Nat, SW.value(X.rem(xw, yw)), Nat.mod(SW.value(xw), V), Nat.mod(SW.value(xw), 1n+bp), DR.divmod_rem(xw, yw, hbzy(y, hzy)), Equal.cong(Nat, Nat, t => Nat.mod(SW.value(xw), t), V, 1n+bp, eBy(y, hzy)))
446  +hq0 = Equal.cong(Nat, Nat, t => Nat.mod(t, 2n), SW.value(X.quot(xw, yw)), Nat.div(SW.value(xw), 1n+bp), Equal.trans(Nat, SW.value(X.quot(xw, yw)), Nat.div(SW.value(xw), V), Nat.div(SW.value(xw), 1n+bp), DQ.divmod_quot(xw, yw, hbzy(y, hzy)), Equal.cong(Nat, Nat, t => Nat.div(SW.value(xw), t), V, 1n+bp, eBy(y, hzy))))
447  +e1 = loop_q(D, yw, bp, eBy(y, hzy), hBy(y, hzy), hbzy(y, hzy), D, N.le_refl(D), X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)), SW.value(xw), hr0, hq0)
448  +e2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.div(C.shift(D, SW.value(xw)), t), 2n), 1n+bp, V, Equal.sym(Nat, V, 1n+bp, eBy(y, hzy)))
449  Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, X.divmod(xw, yw)))), 2n), Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), V), 2n), e0, Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), 1n+bp), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), V), 2n), e1, e2))