Average Error: 0.0 → 0.0
Time: 3.4s
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)\]
↓
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \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)
↓
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(-v \cdot v\right)
double f(double v) {
        double r193321 = 2.0;
        double r193322 = sqrt(r193321);
        double r193323 = 4.0;
        double r193324 = r193322 / r193323;
        double r193325 = 1.0;
        double r193326 = 3.0;
        double r193327 = v;
        double r193328 = r193327 * r193327;
        double r193329 = r193326 * r193328;
        double r193330 = r193325 - r193329;
        double r193331 = sqrt(r193330);
        double r193332 = r193324 * r193331;
        double r193333 = r193325 - r193328;
        double r193334 = r193332 * r193333;
        return r193334;
}
↓
double f(double v) {
        double r193335 = 2.0;
        double r193336 = sqrt(r193335);
        double r193337 = 4.0;
        double r193338 = r193336 / r193337;
        double r193339 = 1.0;
        double r193340 = 3.0;
        double r193341 = v;
        double r193342 = r193341 * r193341;
        double r193343 = r193340 * r193342;
        double r193344 = r193339 - r193343;
        double r193345 = sqrt(r193344);
        double r193346 = r193338 * r193345;
        double r193347 = r193346 * r193339;
        double r193348 = -r193342;
        double r193349 = r193346 * r193348;
        double r193350 = r193347 + r193349;
        return r193350;
}

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 sub-neg0.0

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

  4. Applied distribute-lft-in0.0

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

  5. Final simplification0.0

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

Reproduce

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