Average Error: 0.0 → 0.0
Time: 15.5s
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({1}^{3} - {\left(v \cdot v\right)}^{3}\right) \cdot \frac{\sqrt{2}}{4}}{\frac{{v}^{4} + 1 \cdot \left(v \cdot v + 1\right)}{\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({1}^{3} - {\left(v \cdot v\right)}^{3}\right) \cdot \frac{\sqrt{2}}{4}}{\frac{{v}^{4} + 1 \cdot \left(v \cdot v + 1\right)}{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}}
double f(double v) {
        double r131398 = 2.0;
        double r131399 = sqrt(r131398);
        double r131400 = 4.0;
        double r131401 = r131399 / r131400;
        double r131402 = 1.0;
        double r131403 = 3.0;
        double r131404 = v;
        double r131405 = r131404 * r131404;
        double r131406 = r131403 * r131405;
        double r131407 = r131402 - r131406;
        double r131408 = sqrt(r131407);
        double r131409 = r131401 * r131408;
        double r131410 = r131402 - r131405;
        double r131411 = r131409 * r131410;
        return r131411;
}
↓
double f(double v) {
        double r131412 = 1.0;
        double r131413 = 3.0;
        double r131414 = pow(r131412, r131413);
        double r131415 = v;
        double r131416 = r131415 * r131415;
        double r131417 = pow(r131416, r131413);
        double r131418 = r131414 - r131417;
        double r131419 = 2.0;
        double r131420 = sqrt(r131419);
        double r131421 = 4.0;
        double r131422 = r131420 / r131421;
        double r131423 = r131418 * r131422;
        double r131424 = 4.0;
        double r131425 = pow(r131415, r131424);
        double r131426 = r131416 + r131412;
        double r131427 = r131412 * r131426;
        double r131428 = r131425 + r131427;
        double r131429 = 3.0;
        double r131430 = r131429 * r131416;
        double r131431 = r131412 - r131430;
        double r131432 = sqrt(r131431);
        double r131433 = r131428 / r131432;
        double r131434 = r131423 / r131433;
        return r131434;
}

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 flip3--0.0

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

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

  5. Final simplification0.0

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

Reproduce

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