def nrd_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:467

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

467def nrd_v(+x: F.F64, +y: F.F64) -> {NRd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))) == NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
468  +e1 = Equal.cong(Bool, F.F64, t => NRd(t, F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
469  +e2 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), t, F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
470  +e3 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), t, SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(y), SF.xexp(y), T.dexp_value(y))
471  +e4 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), t, SW.value(F.dmant(y))), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
472  +e5 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), t), SW.value(F.dmant(y)), SF.mant(y), T.dmant_value(y))
473  +r1 = NRd(SF.sign(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
474  +r2 = NRd(SF.sign(x), SF.xexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
475  +r3 = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
476  +r4 = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SW.value(F.dmant(y)))
477  +G = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
478  Equal.trans(F.F64, NRd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, Equal.trans(F.F64, r3, r4, G, e4, e5))))