def rfar_c

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

import Base
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

751def rfar_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +far: Bool, +hfar: {Nat.is_lt(F.dexp(x), F.dexp(y)) == far : Bool}) -> {F.rm_far(x, y, far) == RNs(x, y) : F.F64}:
752  match far:
753    case True{}:
754      rone_c(x, y, h, xlt(x, y, True{}, hfar), Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n), {==})
755    case False{}:
756      +G = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
757      +a1 = RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
758      Equal.trans(F.F64, F.rm_qr(x, y, F.fm_qr(x, y)), a1, RNs(x, y), rm_near_c(x, y, ok_zy(x, y, h)), Equal.trans(F.F64, a1, G, RNs(x, y), rnd_v(x, y), Equal.sym(F.F64, RNs(x, y), G, rn_spec_near(x, y, xlt(x, y, False{}, hfar)))))