Float.below_one: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
Lines 391-435 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=391&end_line=435

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/w64.bend as SW
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/w64.bend as X
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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

# a double Bits{l, hw(E, qh)} with E < k <= 2047 is below Bits{0, H} whose
# high word (without sign) is k * 2^20
def below_one(+l: U32, +qh: U32, +E: Nat, +H: U32, +K: U32, +k: Nat, +hE: {Nat.is_lt(E, k) == True{} : Bool}, +hk: {C.fits(11n, k) == True{} : Bool}, +hn: {F.is_nan(F.Bits{0, H}) == False{} : Bool}, +hz: {F.is_zero(F.Bits{0, H}) == False{} : Bool}, +hs: {F.signbit(F.Bits{0, H}) == False{} : Bool}, +hH: {U32.and(H, 2147483647) == U32.mul(K, X.pow2(20n)) : U32}, +hK: {U32.to_nat(K) == k : Nat}) -> {F.lt(F.Bits{l, hw(E, qh)}, F.Bits{0, H}) == True{} : Bool}:
  +h = hw(E, qh)
  +x = {F.Bits{l, h} : F.F64}
  +y = {F.Bits{0, H} : F.F64}
  +lq = C.low(20n, v(qh))
  +hk2 = WW.lt_of_fits(11n, k, hk)
  +he = N.lt_trans(E, k, 2048n, hE, hk2)
  +hk12 = SH.fits_mono(11n, 12n, k, {==}, hk)
  +vh = hw_value(1n, {==}, E, qh, he)
  +f11 = fits_lt11(E, he)
  +f31 = Equal.trans(Bool, C.fits(31n, v(h)), C.fits(31n, Nat.add(lq, C.shift(20n, E))), True{}, Equal.cong(Nat, Bool, z => C.fits(31n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.limbs_fit(20n, 11n, lq, E, WW.low_fits(20n, v(qh)), f11))
  +ef = Equal.trans(Nat, v(U32.and(U32.div(h, 1048576), 2047)), C.low(11n, C.high(20n, v(h))), E, FB.ef_g(1n, {==}, h, 1048576, {==}, 2047, {==}),
    Equal.trans(Nat, C.low(11n, C.high(20n, v(h))), C.low(11n, E), E,
      Equal.cong(Nat, Nat, z => C.low(11n, z), C.high(20n, v(h)), E, Equal.trans(Nat, C.high(20n, v(h)), C.high(20n, Nat.add(lq, C.shift(20n, E))), E, Equal.cong(Nat, Nat, z => C.high(20n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.high_u(20n, lq, E, WW.low_fits(20n, v(qh))))),
      WW.low_fit(11n, E, f11)))
  +hne = N.is_eq_lt(E, 2047n, N.lt_le_trans(E, k, 2047n, hE, N.lt_succ_le(k, 2047n, hk2)))
  +nanx = Equal.trans(Bool, F.is_nan(x), Bool.and(Nat.is_eq(E, 2047n), F.nz(F.frac(x))), False{},
    Equal.cong(Nat, Bool, z => Bool.and(Nat.is_eq(z, 2047n), F.nz(F.frac(x))), v(U32.and(U32.div(h, 1048576), 2047)), E, ef),
    Equal.cong(Bool, Bool, z => Bool.and(z, F.nz(F.frac(x))), Nat.is_eq(E, 2047n), False{}, hne))
  +uo = Equal.trans(Bool, F.unordered(x, y), Bool.or(False{}, F.is_nan(y)), False{}, Equal.cong(Bool, Bool, z => Bool.or(z, F.is_nan(y)), F.is_nan(x), False{}, nanx), hn)
  +zs = Equal.trans(Bool, F.zeros(x, y), Bool.and(F.is_zero(x), False{}), False{}, Equal.cong(Bool, Bool, z => Bool.and(F.is_zero(x), z), F.is_zero(y), False{}, hz), and_f(F.is_zero(x)))
  +sx = Equal.trans(Bool, F.signbit(x), SF.sign(x), False{}, FB.signbit_g(1n, {==}, l, h, 2147483648, {==}),
    Equal.cong(Bool, Bool, z => Bool.not(z), C.fits(31n, v(h)), True{}, f31))
  +vmx = Equal.trans(Nat, SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))), Nat.add(v(l), C.shift(32n, v(h))),
    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2147483647)), C.low(31n, v(h)), FB.andm(h, 31n, 2147483647, {==})),
    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), C.low(31n, v(h)), v(h), WW.low_fit(31n, v(h), f31)))
  +vmy = Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.and(H, 2147483647)), C.shift(20n, k), hv_one(H, K, k, hk12, hH, hK))
  +hvh = Equal.trans(Bool, Nat.is_lt(v(h), C.shift(20n, k)), Nat.is_lt(Nat.add(lq, C.shift(20n, E)), C.shift(20n, k)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, C.shift(20n, k)), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.lt_hi(20n, lq, E, 0n, k, WW.low_fits(20n, v(qh)), hE))
  +hlt = WW.lt_hi(32n, v(l), v(h), 0n, C.shift(20n, k), LW.vb(l), hvh)
  +cmp = Equal.trans(Bool, X.lt(F.mag(x), F.mag(y)), Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), True{}, WA.lt_value(F.mag(x), F.mag(y)),
    Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))), True{},
      Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))),
        Equal.cong(Nat, Bool, z => Nat.is_lt(z, SW.value(F.mag(y))), SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, v(h))), vmx),
        Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), z), SW.value(F.mag(y)), C.shift(32n, C.shift(20n, k)), vmy)),
      hlt))
  +c1 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, z, F.zeros(x, y)), F.unordered(x, y), False{}, uo)
  +c2 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, False{}, z), F.zeros(x, y), False{}, zs)
  +c3 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, z, F.signbit(y)), F.signbit(x), False{}, sx)
  +c4 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, False{}, z), F.signbit(y), False{}, hs)
  Equal.trans(Bool, F.lt(x, y), F.lt_z(x, y, False{}, F.zeros(x, y)), True{}, c1,
    Equal.trans(Bool, F.lt_z(x, y, False{}, F.zeros(x, y)), F.lt_z(x, y, False{}, False{}), True{}, c2,
      Equal.trans(Bool, F.lt_s(x, y, F.signbit(x), F.signbit(y)), F.lt_s(x, y, False{}, F.signbit(y)), True{}, c3,
        Equal.trans(Bool, F.lt_s(x, y, False{}, F.signbit(y)), F.lt_s(x, y, False{}, False{}), True{}, c4, cmp))))

Uses (57):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=is_eq_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=and_f
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=fits_lt11
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hv_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hw_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=andm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=ef_g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=signbit_g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=vb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=lt_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=limbs_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_hi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_of_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sign
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=frac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=is_nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=lt_s
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=lt_z
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=mag
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=nz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=signbit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=unordered
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=zeros
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=pow2