Average Error: 0.0 → 0.0
Time: 4.2s
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(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}\]
\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(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}
double f(double v) {
        double r302512 = 2.0;
        double r302513 = sqrt(r302512);
        double r302514 = 4.0;
        double r302515 = r302513 / r302514;
        double r302516 = 1.0;
        double r302517 = 3.0;
        double r302518 = v;
        double r302519 = r302518 * r302518;
        double r302520 = r302517 * r302519;
        double r302521 = r302516 - r302520;
        double r302522 = sqrt(r302521);
        double r302523 = r302515 * r302522;
        double r302524 = r302516 - r302519;
        double r302525 = r302523 * r302524;
        return r302525;
}
↓
double f(double v) {
        double r302526 = 2.0;
        double r302527 = sqrt(r302526);
        double r302528 = 4.0;
        double r302529 = r302527 / r302528;
        double r302530 = 1.0;
        double r302531 = 3.0;
        double r302532 = v;
        double r302533 = r302532 * r302532;
        double r302534 = r302531 * r302533;
        double r302535 = r302530 - r302534;
        double r302536 = sqrt(r302535);
        double r302537 = r302529 * r302536;
        double r302538 = r302530 * r302530;
        double r302539 = r302533 * r302533;
        double r302540 = r302538 - r302539;
        double r302541 = r302537 * r302540;
        double r302542 = r302530 + r302533;
        double r302543 = r302541 / r302542;
        return r302543;
}

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

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

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

  5. Final simplification0.0

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

Reproduce

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