def fx_nz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:139

import Base
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/natural.bend as M
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/w64clz.bend as CZ
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

139def fx_nz(+x: F.F64) -> {F.fx_fin(x, F.dmant(x), Nat.sub(64n, X.clz(F.dmant(x)))) == FIN(x) : F.F64 & F.Exp}:
140  +w = F.dmant(x)
141  +V = SW.value(w)
142  +B = M.bit_length(V)
143  +hB = BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==})
144  +eb = Equal.trans(Nat, Nat.sub(64n, X.clz(w)), Nat.sub(64n, Nat.sub(64n, B)), B, Equal.cong(Nat, Nat, t => Nat.sub(64n, t), X.clz(w), Nat.sub(64n, B), CZ.clz_value(w)), T.subsub(64n, B, N.le_trans(B, 53n, 64n, hB, {==})))
145  +e0 = Equal.cong(Nat, F.F64 & F.Exp, b => F.fx_fin(x, w, b), Nat.sub(64n, X.clz(w)), B, eb)
146  +hx = RT.le_sub(63n, B, 3000n, N.le_trans(B, 53n, 2937n, BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==}), {==}))
147  +a1 = T.rw_value(F.signbit(x), Nat.sub(3000n, B), w, hx)
148  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, V, Nat.sub(3000n, B)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
149  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, Nat.sub(3000n, M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
150  +A0 = F.round_w(F.signbit(x), Nat.sub(3000n, B), w)
151  +A1 = SF.round(F.signbit(x), V, Nat.sub(3000n, B))
152  +A2 = SF.round(SF.sign(x), V, Nat.sub(3000n, B))
153  +A3 = SF.round(SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), M.bit_length(SF.mant(x))))
154  +ea = Equal.trans(F.F64, A0, A1, A3, a1, Equal.trans(F.F64, A1, A2, A3, a2, a3))
155  +b1 = exp_eq(Nat.add(F.dexp(x), B))
156  +b2 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(t, B)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
157  +b3 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
158  +B0 = F.exp_of(Nat.add(F.dexp(x), B))
159  +B1 = SF.exp_of(Nat.add(F.dexp(x), B))
160  +B2 = SF.exp_of(Nat.add(SF.xexp(x), B))
161  +B3 = SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(SF.mant(x))))
162  +eb2 = Equal.trans(F.Exp, B0, B1, B3, b1, Equal.trans(F.Exp, B1, B2, B3, b2, b3))
163  +p1 = Equal.cong(F.F64, F.F64 & F.Exp, t => (t, B0), A0, A3, ea)
164  +p2 = Equal.cong(F.Exp, F.F64 & F.Exp, t => (A3, t), B0, B3, eb2)
165  Equal.trans(F.F64 & F.Exp, F.fx_fin(x, w, Nat.sub(64n, X.clz(w))), F.fx_fin(x, w, B), FIN(x), e0, Equal.trans(F.F64 & F.Exp, (A0, B0), (A3, B0), FIN(x), p1, p2))