def big54

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

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

693def big54(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.is_eq(Nat.sub(SF.xexp(y), SF.xexp(x)), 1n) == False{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y)), Nat.add(SF.mant(x), SF.mant(x))) == False{} : Bool}:
694  +k = Nat.sub(SF.xexp(y), SF.xexp(x))
695  +S = C.shift(k, SF.mant(y))
696  +m2 = Nat.add(SF.mant(x), SF.mant(x))
697  +hk2 = two_le(k, FR.lt_sub_pos(SF.xexp(x), SF.xexp(y), hlt), hk)
698  +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, yn_c(x, y, hlt, Nat.is_eq(SF.efield(y), 0n), {==})))
699  +h54 = Equal.trans(Bool, Nat.is_le(Nat.add(2n, 52n), Nat.add(k, 52n)), Nat.is_le(2n, k), True{}, FR.le_cancel_r(2n, k, 52n), hk2)
700  +f2 = FL.nfit_mono(54n, Nat.add(k, 52n), S, h54, f1)
701  +f3 = FR.fits_add1(53n, SF.mant(x), SF.mant(x), T.mant_fits(x), T.mant_fits(x))
702  +l1 = Equal.trans(Bool, Nat.is_lt(m2, C.shift(54n, one)), C.fits(54n, m2), True{}, FR.lt_fit(54n, one, h1, m2), f3)
703  +l2 = Equal.trans(Bool, Nat.is_le(C.shift(54n, one), S), Bool.not(C.fits(54n, S)), True{}, FB.le_fit(54n, one, h1, S), Equal.cong(Bool, Bool, b => Bool.not(b), C.fits(54n, S), False{}, f2))
704  N.le_not_lt(S, m2, N.lt_le(m2, S, N.lt_le_trans(m2, C.shift(54n, one), S, l1, l2)))