def rnd_v

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

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

610def rnd_v(+x: F.F64, +y: F.F64) -> {RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))) == RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
611  +e1 = Equal.cong(Bool, F.F64, t => RNd(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))
612  +e2 = Equal.cong(Nat, F.F64, t => RNd(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))
613  +e3 = Equal.cong(Nat, F.F64, t => RNd(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))
614  +e4 = Equal.cong(Nat, F.F64, t => RNd(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))
615  +e5 = Equal.cong(Nat, F.F64, t => RNd(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))
616  +r1 = RNd(SF.sign(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
617  +r2 = RNd(SF.sign(x), SF.xexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
618  +r3 = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
619  +r4 = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SW.value(F.dmant(y)))
620  +G = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
621  Equal.trans(F.F64, RNd(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))))