def n1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64norm.bend:102

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

102# the normalized significand
103def 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}:
104  match ea:
105    case 0n:
106      +ez = ez0(E, hea)
107      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
108      +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))
109      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)))
110    case 1n+ +p:
111      +ez = ezs(p, E, hea)
112      +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))
113      +em = Equal.cong(Nat, Nat, z => Nat.add(Fr, C.shift(52n, z)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, ec)
114      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
115      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)))