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{\left(\sqrt{2} \cdot \sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\left({v}^{2} \cdot \left({v}^{2} + 1\right) + 1 \cdot 1\right) \cdot \left(4 \cdot \sqrt{1 + 3 \cdot \left(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{\left(\sqrt{2} \cdot \sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\left({v}^{2} \cdot \left({v}^{2} + 1\right) + 1 \cdot 1\right) \cdot \left(4 \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\right)}
double f(double v) {
        double r145595 = 2.0;
        double r145596 = sqrt(r145595);
        double r145597 = 4.0;
        double r145598 = r145596 / r145597;
        double r145599 = 1.0;
        double r145600 = 3.0;
        double r145601 = v;
        double r145602 = r145601 * r145601;
        double r145603 = r145600 * r145602;
        double r145604 = r145599 - r145603;
        double r145605 = sqrt(r145604);
        double r145606 = r145598 * r145605;
        double r145607 = r145599 - r145602;
        double r145608 = r145606 * r145607;
        return r145608;
}
↓
double f(double v) {
        double r145609 = 2.0;
        double r145610 = sqrt(r145609);
        double r145611 = 1.0;
        double r145612 = r145611 * r145611;
        double r145613 = 3.0;
        double r145614 = v;
        double r145615 = r145614 * r145614;
        double r145616 = r145613 * r145615;
        double r145617 = r145616 * r145616;
        double r145618 = r145612 - r145617;
        double r145619 = sqrt(r145618);
        double r145620 = r145610 * r145619;
        double r145621 = 3.0;
        double r145622 = pow(r145611, r145621);
        double r145623 = pow(r145615, r145621);
        double r145624 = r145622 - r145623;
        double r145625 = r145620 * r145624;
        double r145626 = 2.0;
        double r145627 = pow(r145614, r145626);
        double r145628 = r145627 + r145611;
        double r145629 = r145627 * r145628;
        double r145630 = r145629 + r145612;
        double r145631 = 4.0;
        double r145632 = r145611 + r145616;
        double r145633 = sqrt(r145632);
        double r145634 = r145631 * r145633;
        double r145635 = r145630 * r145634;
        double r145636 = r145625 / r145635;
        return r145636;
}

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

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \sqrt{\color{blue}{\frac{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \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)}\]

  5. Applied sqrt-div0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \color{blue}{\frac{\sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \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)}\]

  6. Applied frac-times0.0

    \[\leadsto \color{blue}{\frac{\sqrt{2} \cdot \sqrt{1 \cdot 1 - \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)}}{4 \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}}} \cdot \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)}\]

  7. Applied frac-times0.0

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

  8. Simplified0.0

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

  9. Final simplification0.0

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

Reproduce

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