def iq_eps

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:135

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

135# the remainder e = (a - b) * 2^62 - h * b, and 4 e = low2(Q) * b + r2
136def iq_eps(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))) == Nat.add(Nat.mul(C.low(2n, Q), B), r2) : Nat}:
137  +p = iq_parts(B, R, Q, r2, hQ)
138  +e1 = N.sub_add(C.shift(62n, R), Nat.mul(C.high(2n, Q), B), iq_le(B, R, Q, r2, hQ))
139  +e2 = Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), WW.shift_add(2n, Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Equal.cong(Nat, Nat, z => C.shift(2n, z), Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), C.shift(62n, R), e1))
140  NR.add_cancel(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), Nat.add(Nat.mul(C.low(2n, Q), B), r2), Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), e2, Equal.sym(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p)))