def far_lt

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

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

357# y's significand moved up by k >= 1 is at least 2^53 > mant(x)
358def far_lt(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(SF.mant(x), C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y))) == True{} : Bool}:
359  +k = Nat.sub(SF.xexp(y), SF.xexp(x))
360  +S = C.shift(k, SF.mant(y))
361  +hk = FR.lt_sub_pos(SF.xexp(x), SF.xexp(y), hlt)
362  +hy = yn_c(x, y, hlt, Nat.is_eq(SF.efield(y), 0n), {==})
363  +f1 = Equal.trans(Bool, C.fits(Nat.add(k, 52n), S), C.fits(52n, SF.mant(y)), False{}, RT.fits_sh(k, 52n, SF.mant(y)), nf52(y, hy))
364  +h53 = Equal.trans(Bool, Nat.is_le(Nat.add(1n, 52n), Nat.add(k, 52n)), Nat.is_le(1n, k), True{}, FR.le_cancel_r(1n, k, 52n), hk)
365  +f2 = FL.nfit_mono(53n, Nat.add(k, 52n), S, h53, f1)
366  +l1 = Equal.trans(Bool, Nat.is_lt(SF.mant(x), C.shift(53n, one)), C.fits(53n, SF.mant(x)), True{}, FR.lt_fit(53n, one, h1, SF.mant(x)), T.mant_fits(x))
367  +l2 = Equal.trans(Bool, Nat.is_le(C.shift(53n, one), S), Bool.not(C.fits(53n, S)), True{}, FB.le_fit(53n, one, h1, S), Equal.cong(Bool, Bool, b => Bool.not(b), C.fits(53n, S), False{}, f2))
368  N.lt_le_trans(SF.mant(x), C.shift(53n, one), S, l1, l2)