Fround.enc_bits: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
Lines 33-42 of bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&start_line=33&end_line=42

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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

def enc_bits(+s: Bool, +ef: Nat, +f: Nat) -> {SF.encode(s, ef, f) == bits(s, Nat.add(f, C.shift(52n, ef))) : F.F64}:
  +t = C.shift(20n, ef)
  +n = Nat.add(f, C.shift(52n, ef))
  +b = C.shift(31n, SF.b2n(s))
  +e52 = WW.shift_comp(32n, 20n, ef)
  +el = Equal.trans(Nat, C.low(32n, n), C.low(32n, Nat.add(f, C.shift(32n, t))), C.low(32n, f), Equal.cong(Nat, Nat, z => C.low(32n, Nat.add(f, z)), C.shift(52n, ef), C.shift(32n, t), e52), WW.low_add_shift(32n, f, t))
  +eh0 = Equal.trans(Nat, C.high(32n, n), C.high(32n, Nat.add(f, C.shift(32n, t))), Nat.add(C.high(32n, f), t), Equal.cong(Nat, Nat, z => C.high(32n, Nat.add(f, z)), C.shift(52n, ef), C.shift(32n, t), e52), WW.high_add_shift(32n, f, t))
  +eh = Equal.trans(Nat, Nat.add(C.high(32n, n), b), Nat.add(Nat.add(C.high(32n, f), t), b), Nat.add(C.high(32n, f), C.shift(20n, Nat.add(ef, C.shift(11n, SF.b2n(s))))), Equal.cong(Nat, Nat, z => Nat.add(z, b), C.high(32n, n), Nat.add(C.high(32n, f), t), eh0), FB.fold(C.high(32n, f), ef, SF.b2n(s)))
  +e = Equal.trans(F.F64, bits(s, n), F.Bits{U32.from_nat(C.low(32n, f)), U32.from_nat(Nat.add(C.high(32n, n), b))}, SF.encode(s, ef, f), Equal.cong(Nat, F.F64, z => F.Bits{U32.from_nat(z), U32.from_nat(Nat.add(C.high(32n, n), b))}, C.low(32n, n), C.low(32n, f), el), Equal.cong(Nat, F.F64, z => F.Bits{U32.from_nat(C.low(32n, f)), U32.from_nat(z)}, Nat.add(C.high(32n, n), b), Nat.add(C.high(32n, f), C.shift(20n, Nat.add(ef, C.shift(11n, SF.b2n(s))))), eh))
  Equal.sym(F.F64, bits(s, n), SF.encode(s, ef, f), e)

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.sym
  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=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=fold
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_add_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_add_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp
  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=b2n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64