def rm_many

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

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/src/math/f64.bend as F
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/f64round.bend as FR

709# two or more scale steps below y: x itself
710def rm_many(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n) == False{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {RNs(x, y) == x : F.F64}:
711  +s = SF.sign(x)
712  +xx = SF.xexp(x)
713  +mx = SF.mant(x)
714  +S = C.shift(Nat.sub(SF.xexp(y), xx), SF.mant(y))
715  +hk2 = L.subst(Nat, t => {Nat.is_eq(t, 1n) == False{} : Bool}, Nat.sub(F.dexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), xx), xsub(x, y), hk)
716  +fl = or_ff(Nat.is_lt(S, Nat.add(mx, mx)), Bool.and(Nat.is_eq(Nat.add(mx, mx), S), False{}), big54(x, y, hlt, hk2, 1n, {==}), FR.and_f(Nat.is_eq(Nat.add(mx, mx), S)))
717  +e1 = rn_spec_far(x, y, hlt)
718  +e2 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.round(Bool.not(s), Nat.sub(S, mx), xx), SF.round(s, mx, xx)), SF.rflip(mx, S, 0n), False{}, fl)
719  Equal.trans(F.F64, RNs(x, y), SF.rnear(s, mx, S, 0n, xx), x, e1, Equal.trans(F.F64, SF.rnear(s, mx, S, 0n, xx), SF.round(s, mx, xx), x, e2, rt(x, hfin)))