def small_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ratio.bend:58

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/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
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/f64tools.bend as T

58def small_v(+x: F.F64) -> {SF.rtriple(F.ar_small(F.signbit(x), F.dmant(x), Nat.sub(3000n, F.dexp(x)), Nat.min(F.ctz(F.dmant(x)), Nat.sub(3000n, F.dexp(x))))) == SMALL(x) : Result<&2, &2, NE.NumError, SF.Rat>}:
59  +w = F.dmant(x)
60  +V = SW.value(w)
61  +k = Nat.sub(3000n, F.dexp(x))
62  +j = Nat.min(F.ctz(w), k)
63  +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => Done{SF.Rat{F.signbit(x), t, Nat.sub(k, j)}}, SW.value(X.shr(w, j)), C.high(j, V), SH.shr_value(w, j))
64  +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(F.signbit(x), V, k, Nat.min(t, k)), F.ctz(w), SF.tz(64n, V), ctz_v(w))
65  +e3 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, t => G(t, V, k, Nat.min(SF.tz(64n, V), k)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
66  +e4 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(SF.sign(x), t, k, Nat.min(SF.tz(64n, t), k)), V, SF.mant(x), T.dmant_value(x))
67  +e5 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(SF.sign(x), SF.mant(x), Nat.sub(3000n, t), Nat.min(SF.tz(64n, SF.mant(x)), Nat.sub(3000n, t))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
68  +r1 = G(F.signbit(x), V, k, j)
69  +r2 = G(F.signbit(x), V, k, Nat.min(SF.tz(64n, V), k))
70  +r3 = G(SF.sign(x), V, k, Nat.min(SF.tz(64n, V), k))
71  +r4 = G(SF.sign(x), SF.mant(x), k, Nat.min(SF.tz(64n, SF.mant(x)), k))
72  Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, Done{SF.Rat{F.signbit(x), SW.value(X.shr(w, j)), Nat.sub(k, j)}}, r1, SMALL(x), e1, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r1, r2, SMALL(x), e2, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r2, r3, SMALL(x), e3, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r3, r4, SMALL(x), e4, e5))))