Average Error: 0.0 → 0.0
Time: 37.3s
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(\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(\sqrt{1} + v\right)\right) \cdot \left(\sqrt{1} - 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(\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(\sqrt{1} + v\right)\right) \cdot \left(\sqrt{1} - v\right)
double f(double v) {
        double r534272 = 2.0;
        double r534273 = sqrt(r534272);
        double r534274 = 4.0;
        double r534275 = r534273 / r534274;
        double r534276 = 1.0;
        double r534277 = 3.0;
        double r534278 = v;
        double r534279 = r534278 * r534278;
        double r534280 = r534277 * r534279;
        double r534281 = r534276 - r534280;
        double r534282 = sqrt(r534281);
        double r534283 = r534275 * r534282;
        double r534284 = r534276 - r534279;
        double r534285 = r534283 * r534284;
        return r534285;
}
↓
double f(double v) {
        double r534286 = 2.0;
        double r534287 = sqrt(r534286);
        double r534288 = 4.0;
        double r534289 = r534287 / r534288;
        double r534290 = 1.0;
        double r534291 = 3.0;
        double r534292 = v;
        double r534293 = r534292 * r534292;
        double r534294 = r534291 * r534293;
        double r534295 = r534290 - r534294;
        double r534296 = sqrt(r534295);
        double r534297 = r534289 * r534296;
        double r534298 = sqrt(r534290);
        double r534299 = r534298 + r534292;
        double r534300 = r534297 * r534299;
        double r534301 = r534298 - r534292;
        double r534302 = r534300 * r534301;
        return r534302;
}

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 add-sqr-sqrt0.0

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

  4. Applied difference-of-squares0.0

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

  5. Applied associate-*r*0.0

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

  6. Final simplification0.0

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

Reproduce

herbie shell --seed 2020036 +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))))