def fm_far

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

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/nat.bend as N

373# the spec's operands when x has the smaller scale
374def fm_far(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {FM(x, y) == x : F.F64}:
375  +s = SF.sign(x)
376  +xx = SF.xexp(x)
377  +xy = SF.xexp(y)
378  +mx = SF.mant(x)
379  +my = SF.mant(y)
380  +S = C.shift(Nat.sub(xy, xx), my)
381  +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xx, N.min_left(xx, xy, hlt))
382  +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(t, mx), S), xx), Nat.sub(xx, xx), 0n, N.sub_self(xx))
383  +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, t, xx), Nat.mod(mx, S), mx, mod_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
384  +r1 = SF.round(s, Nat.mod(C.shift(Nat.sub(xx, xx), mx), S), xx)
385  +r2 = SF.round(s, Nat.mod(mx, S), xx)
386  Equal.trans(F.F64, FM(x, y), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, SF.round(s, mx, xx), x, e3, rt(x, hfin))))