Average Error: 0.0 → 0.0
Time: 4.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)\]
↓
\[\frac{\left(\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\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 4}\]
\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 - 3 \cdot \left(v \cdot v\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 4}
double f(double v) {
        double r230592 = 2.0;
        double r230593 = sqrt(r230592);
        double r230594 = 4.0;
        double r230595 = r230593 / r230594;
        double r230596 = 1.0;
        double r230597 = 3.0;
        double r230598 = v;
        double r230599 = r230598 * r230598;
        double r230600 = r230597 * r230599;
        double r230601 = r230596 - r230600;
        double r230602 = sqrt(r230601);
        double r230603 = r230595 * r230602;
        double r230604 = r230596 - r230599;
        double r230605 = r230603 * r230604;
        return r230605;
}
↓
double f(double v) {
        double r230606 = 2.0;
        double r230607 = sqrt(r230606);
        double r230608 = 1.0;
        double r230609 = 3.0;
        double r230610 = v;
        double r230611 = r230610 * r230610;
        double r230612 = r230609 * r230611;
        double r230613 = r230608 - r230612;
        double r230614 = sqrt(r230613);
        double r230615 = r230607 * r230614;
        double r230616 = 3.0;
        double r230617 = pow(r230608, r230616);
        double r230618 = pow(r230611, r230616);
        double r230619 = r230617 - r230618;
        double r230620 = r230615 * r230619;
        double r230621 = 2.0;
        double r230622 = pow(r230610, r230621);
        double r230623 = r230622 + r230608;
        double r230624 = r230622 * r230623;
        double r230625 = r230608 * r230608;
        double r230626 = r230624 + r230625;
        double r230627 = 4.0;
        double r230628 = r230626 * r230627;
        double r230629 = r230620 / r230628;
        return r230629;
}

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

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

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

  6. Simplified0.0

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

  7. Final simplification0.0

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

Reproduce

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