Average Error: 0.0 → 0.0
Time: 14.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(1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)\right) \cdot \sqrt{1 - \left(v \cdot 3\right) \cdot v}}{\left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + v \cdot v\right) + 1} \cdot \frac{\sqrt{2}}{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(1 - \left(v \cdot \left(v \cdot v\right)\right) \cdot \left(v \cdot \left(v \cdot v\right)\right)\right) \cdot \sqrt{1 - \left(v \cdot 3\right) \cdot v}}{\left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + v \cdot v\right) + 1} \cdot \frac{\sqrt{2}}{4}
double f(double v) {
        double r4002704 = 2.0;
        double r4002705 = sqrt(r4002704);
        double r4002706 = 4.0;
        double r4002707 = r4002705 / r4002706;
        double r4002708 = 1.0;
        double r4002709 = 3.0;
        double r4002710 = v;
        double r4002711 = r4002710 * r4002710;
        double r4002712 = r4002709 * r4002711;
        double r4002713 = r4002708 - r4002712;
        double r4002714 = sqrt(r4002713);
        double r4002715 = r4002707 * r4002714;
        double r4002716 = r4002708 - r4002711;
        double r4002717 = r4002715 * r4002716;
        return r4002717;
}
↓
double f(double v) {
        double r4002718 = 1.0;
        double r4002719 = v;
        double r4002720 = r4002719 * r4002719;
        double r4002721 = r4002719 * r4002720;
        double r4002722 = r4002721 * r4002721;
        double r4002723 = r4002718 - r4002722;
        double r4002724 = 3.0;
        double r4002725 = r4002719 * r4002724;
        double r4002726 = r4002725 * r4002719;
        double r4002727 = r4002718 - r4002726;
        double r4002728 = sqrt(r4002727);
        double r4002729 = r4002723 * r4002728;
        double r4002730 = r4002720 * r4002720;
        double r4002731 = r4002730 + r4002720;
        double r4002732 = r4002731 + r4002718;
        double r4002733 = r4002729 / r4002732;
        double r4002734 = 2.0;
        double r4002735 = sqrt(r4002734);
        double r4002736 = 4.0;
        double r4002737 = r4002735 / r4002736;
        double r4002738 = r4002733 * r4002737;
        return r4002738;
}

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. Using strategy rm

  5. Applied flip3--0.0

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

  6. Applied associate-*r/0.0

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

  7. Simplified0.0

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

  8. Final simplification0.0

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

Reproduce

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