Average Error: 0.0 → 0.0
Time: 20.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)\]
↓
\[\left(\sqrt{1} - v\right) \cdot \left(\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\sqrt{1} + 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)
↓
\left(\sqrt{1} - v\right) \cdot \left(\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\sqrt{1} + v\right)\right)
double f(double v) {
        double r7368874 = 2.0;
        double r7368875 = sqrt(r7368874);
        double r7368876 = 4.0;
        double r7368877 = r7368875 / r7368876;
        double r7368878 = 1.0;
        double r7368879 = 3.0;
        double r7368880 = v;
        double r7368881 = r7368880 * r7368880;
        double r7368882 = r7368879 * r7368881;
        double r7368883 = r7368878 - r7368882;
        double r7368884 = sqrt(r7368883);
        double r7368885 = r7368877 * r7368884;
        double r7368886 = r7368878 - r7368881;
        double r7368887 = r7368885 * r7368886;
        return r7368887;
}
↓
double f(double v) {
        double r7368888 = 1.0;
        double r7368889 = sqrt(r7368888);
        double r7368890 = v;
        double r7368891 = r7368889 - r7368890;
        double r7368892 = r7368890 * r7368890;
        double r7368893 = 3.0;
        double r7368894 = r7368892 * r7368893;
        double r7368895 = r7368888 - r7368894;
        double r7368896 = sqrt(r7368895);
        double r7368897 = 2.0;
        double r7368898 = sqrt(r7368897);
        double r7368899 = 4.0;
        double r7368900 = r7368898 / r7368899;
        double r7368901 = r7368896 * r7368900;
        double r7368902 = r7368889 + r7368890;
        double r7368903 = r7368901 * r7368902;
        double r7368904 = r7368891 * r7368903;
        return r7368904;
}

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

Reproduce

herbie shell --seed 2019172 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))