F64norm.n1: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as F64norm
Lines 102-115 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&start_line=102&end_line=115

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/spec/math/w64.bend as SW
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/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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

# the normalized significand
def n1(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {SW.value(F.norm_f(ea, fa)) == C.shift(sa(ea, fa), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))) : Nat}:
  match ea:
    case 0n:
      +ez = ez0(E, hea)
      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
      +em = Equal.trans(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, 0n), Fr, Equal.cong(Bool, Nat, t => Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(E, 0n), True{}, ez), N.add_zero(Fr))
      Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), C.shift(Nat.sub(X.clz(fa), 11n), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n)))))), sub_val(fa, Fr, hfa, hF, hz), Equal.cong(Nat, Nat, z => C.shift(Nat.sub(X.clz(fa), 11n), z), Fr, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Fr, em)))
    case 1n+ +p:
      +ez = ezs(p, E, hea)
      +ec = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(E, 0n))), 1n, one, Equal.cong(Bool, Nat, t => SF.b2n(Bool.not(t)), Nat.is_eq(E, 0n), False{}, ez), Equal.sym(Nat, one, 1n, h1))
      +em = Equal.cong(Nat, Nat, z => Nat.add(Fr, C.shift(52n, z)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, ec)
      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
      Equal.trans(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), hid(one, h1, fa, hFv, 1048576, {==}), Equal.trans(Nat, Nat.add(SW.value(fa), C.shift(52n, one)), Nat.add(Fr, C.shift(52n, one)), Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, one)), SW.value(fa), Fr, hfa), Equal.sym(Nat, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(E, 0n))))), Nat.add(Fr, C.shift(52n, one)), em)))

Uses (26):
  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=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=Nat.is_eq
  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/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&name=ez0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&name=ezs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&name=hid
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&name=sa
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend&name=sub_val
  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=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/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=norm_f
  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=add
  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