Average Error: 0.0 → 0.0
Time: 11.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({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 r171364 = 2.0;
        double r171365 = sqrt(r171364);
        double r171366 = 4.0;
        double r171367 = r171365 / r171366;
        double r171368 = 1.0;
        double r171369 = 3.0;
        double r171370 = v;
        double r171371 = r171370 * r171370;
        double r171372 = r171369 * r171371;
        double r171373 = r171368 - r171372;
        double r171374 = sqrt(r171373);
        double r171375 = r171367 * r171374;
        double r171376 = r171368 - r171371;
        double r171377 = r171375 * r171376;
        return r171377;
}
↓
double f(double v) {
        double r171378 = 1.0;
        double r171379 = 3.0;
        double r171380 = pow(r171378, r171379);
        double r171381 = v;
        double r171382 = r171381 * r171381;
        double r171383 = pow(r171382, r171379);
        double r171384 = r171380 - r171383;
        double r171385 = 2.0;
        double r171386 = sqrt(r171385);
        double r171387 = 4.0;
        double r171388 = r171386 / r171387;
        double r171389 = r171384 * r171388;
        double r171390 = 4.0;
        double r171391 = pow(r171381, r171390);
        double r171392 = r171382 + r171378;
        double r171393 = r171378 * r171392;
        double r171394 = r171391 + r171393;
        double r171395 = 3.0;
        double r171396 = r171395 * r171382;
        double r171397 = r171378 - r171396;
        double r171398 = sqrt(r171397);
        double r171399 = r171394 / r171398;
        double r171400 = r171389 / r171399;
        return r171400;
}

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 2019304 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))