Average Error: 0.0 → 0.0
Time: 3.8s
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{\sqrt{2}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)\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{\sqrt{2}}{4} \cdot \left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)\right)
double f(double v) {
        double r323290 = 2.0;
        double r323291 = sqrt(r323290);
        double r323292 = 4.0;
        double r323293 = r323291 / r323292;
        double r323294 = 1.0;
        double r323295 = 3.0;
        double r323296 = v;
        double r323297 = r323296 * r323296;
        double r323298 = r323295 * r323297;
        double r323299 = r323294 - r323298;
        double r323300 = sqrt(r323299);
        double r323301 = r323293 * r323300;
        double r323302 = r323294 - r323297;
        double r323303 = r323301 * r323302;
        return r323303;
}
↓
double f(double v) {
        double r323304 = 2.0;
        double r323305 = sqrt(r323304);
        double r323306 = 4.0;
        double r323307 = r323305 / r323306;
        double r323308 = 1.0;
        double r323309 = 3.0;
        double r323310 = v;
        double r323311 = r323310 * r323310;
        double r323312 = r323309 * r323311;
        double r323313 = r323308 - r323312;
        double r323314 = sqrt(r323313);
        double r323315 = r323308 - r323311;
        double r323316 = r323314 * r323315;
        double r323317 = r323307 * r323316;
        return r323317;
}

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 associate-*l*0.0

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

  4. Final simplification0.0

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

Reproduce

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