Float.impl_eq: 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 251-265 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=251&end_line=265

import Base
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/random/rand.bend as R
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/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC

# the implementation: shift by 52 - j, exponent field j + 970, for the bit
# length 1 + j of the significand (j a variable, so no bit length is ever
# evaluated inside a comparison)
def impl_eq(+m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {R.f53(m, X.clz(m)) == bits(X.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) : F.F64}:
  +r = Nat.sub(52n, j)
  +E = Nat.add(j, 970n)
  +c = X.clz(m)
  +hclz = Equal.trans(Nat, c, Nat.sub(64n, M.bit_length(SW.value(m))), Nat.sub(63n, j), WC.clz_value(m),
    Equal.trans(Nat, Nat.sub(64n, M.bit_length(SW.value(m))), Nat.sub(64n, M.bit_length(1n+np)), Nat.sub(63n, j), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(m), 1n+np, hM), Equal.cong(Nat, Nat, z => Nat.sub(64n, z), M.bit_length(1n+np), 1n+j, hbl)))
  +es = Equal.trans(Nat, Nat.sub(c, 11n), Nat.sub(Nat.sub(63n, j), 11n), r, Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), c, Nat.sub(63n, j), hclz), shift_amt(j, hj))
  +ee = Equal.trans(Nat, Nat.sub(1033n, c), Nat.sub(1033n, Nat.sub(63n, j)), E, Equal.cong(Nat, Nat, z => Nat.sub(1033n, z), c, Nat.sub(63n, j), hclz), exp_amt(j, hj))
  +i2 = Equal.cong(Nat, F.F64, z => bits(X.shl(m, z), Nat.sub(1033n, c)), Nat.sub(c, 11n), r, es)
  +i3 = Equal.cong(Nat, F.F64, z => bits(X.shl(m, r), z), Nat.sub(1033n, c), E, ee)
  Equal.trans(F.F64, R.f53(m, c), bits(X.shl(m, Nat.sub(c, 11n)), Nat.sub(1033n, c)), bits(X.shl(m, r), E), {==},
    Equal.trans(F.F64, bits(X.shl(m, Nat.sub(c, 11n)), Nat.sub(1033n, c)), bits(X.shl(m, r), Nat.sub(1033n, c)), bits(X.shl(m, r), E), i2, i3))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=exp_amt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=shift_amt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend&name=clz_value
  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/natural.bend&name=bit_length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=f53
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=clz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shl