Average Error: 0.0 → 0.0
Time: 4.3s
Precision: 64
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
↓
\[\frac{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\frac{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}
double f(double v) {
        double r304254 = 2.0;
        double r304255 = sqrt(r304254);
        double r304256 = 4.0;
        double r304257 = r304255 / r304256;
        double r304258 = 1.0;
        double r304259 = 3.0;
        double r304260 = v;
        double r304261 = r304260 * r304260;
        double r304262 = r304259 * r304261;
        double r304263 = r304258 - r304262;
        double r304264 = sqrt(r304263);
        double r304265 = r304257 * r304264;
        double r304266 = r304258 - r304261;
        double r304267 = r304265 * r304266;
        return r304267;
}
↓
double f(double v) {
        double r304268 = 2.0;
        double r304269 = sqrt(r304268);
        double r304270 = 4.0;
        double r304271 = r304269 / r304270;
        double r304272 = 1.0;
        double r304273 = 3.0;
        double r304274 = v;
        double r304275 = r304274 * r304274;
        double r304276 = r304273 * r304275;
        double r304277 = r304272 - r304276;
        double r304278 = sqrt(r304277);
        double r304279 = r304271 * r304278;
        double r304280 = r304272 * r304272;
        double r304281 = r304275 * r304275;
        double r304282 = r304280 - r304281;
        double r304283 = r304279 * r304282;
        double r304284 = r304272 + r304275;
        double r304285 = r304283 / r304284;
        return r304285;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.0

    \[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
  2. Using strategy rm

  3. Applied flip--0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \color{blue}{\frac{1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)}{1 + v \cdot v}}\]

  4. Applied associate-*r/0.0

    \[\leadsto \color{blue}{\frac{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}}\]

  5. Final simplification0.0

    \[\leadsto \frac{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}\]

Reproduce

herbie shell --seed 2020081 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))