Average Error: 0.0 → 0.0
Time: 5.1s
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(\sqrt{2} \cdot \sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}{4 \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}}\]
\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(\sqrt{2} \cdot \sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}{4 \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}}
double f(double v) {
        double r212361 = 2.0;
        double r212362 = sqrt(r212361);
        double r212363 = 4.0;
        double r212364 = r212362 / r212363;
        double r212365 = 1.0;
        double r212366 = 3.0;
        double r212367 = v;
        double r212368 = r212367 * r212367;
        double r212369 = r212366 * r212368;
        double r212370 = r212365 - r212369;
        double r212371 = sqrt(r212370);
        double r212372 = r212364 * r212371;
        double r212373 = r212365 - r212368;
        double r212374 = r212372 * r212373;
        return r212374;
}
↓
double f(double v) {
        double r212375 = 2.0;
        double r212376 = sqrt(r212375);
        double r212377 = 1.0;
        double r212378 = r212377 * r212377;
        double r212379 = 3.0;
        double r212380 = v;
        double r212381 = r212380 * r212380;
        double r212382 = r212379 * r212381;
        double r212383 = r212382 * r212382;
        double r212384 = r212378 - r212383;
        double r212385 = sqrt(r212384);
        double r212386 = r212376 * r212385;
        double r212387 = r212377 - r212381;
        double r212388 = r212386 * r212387;
        double r212389 = 4.0;
        double r212390 = r212377 + r212382;
        double r212391 = sqrt(r212390);
        double r212392 = r212389 * r212391;
        double r212393 = r212388 / r212392;
        return r212393;
}

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{\color{blue}{\frac{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \left(1 - v \cdot v\right)\]

  4. Applied sqrt-div0.0

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

  5. Applied frac-times0.0

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

  6. Applied associate-*l/0.0

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

  7. Final simplification0.0

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

Reproduce

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