Average Error: 0.0 → 0.0
Time: 25.9s
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{\frac{\sqrt{2}}{4} \cdot \left(\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(3 \cdot \left(v \cdot v\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right)}{\left(v \cdot v + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right) \cdot \sqrt{\left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 3 \cdot \left(v \cdot v\right)\right) + 1} + \sqrt{\left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 3 \cdot \left(v \cdot v\right)\right) + 1}}\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\frac{\frac{\sqrt{2}}{4} \cdot \left(\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(3 \cdot \left(v \cdot v\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}\right)}{\left(v \cdot v + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right) \cdot \sqrt{\left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 3 \cdot \left(v \cdot v\right)\right) + 1} + \sqrt{\left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 3 \cdot \left(v \cdot v\right)\right) + 1}}
double f(double v) {
        double r4818867 = 2.0;
        double r4818868 = sqrt(r4818867);
        double r4818869 = 4.0;
        double r4818870 = r4818868 / r4818869;
        double r4818871 = 1.0;
        double r4818872 = 3.0;
        double r4818873 = v;
        double r4818874 = r4818873 * r4818873;
        double r4818875 = r4818872 * r4818874;
        double r4818876 = r4818871 - r4818875;
        double r4818877 = sqrt(r4818876);
        double r4818878 = r4818870 * r4818877;
        double r4818879 = r4818871 - r4818874;
        double r4818880 = r4818878 * r4818879;
        return r4818880;
}
↓
double f(double v) {
        double r4818881 = 2.0;
        double r4818882 = sqrt(r4818881);
        double r4818883 = 4.0;
        double r4818884 = r4818882 / r4818883;
        double r4818885 = 1.0;
        double r4818886 = v;
        double r4818887 = r4818886 * r4818886;
        double r4818888 = r4818886 * r4818887;
        double r4818889 = r4818888 * r4818888;
        double r4818890 = r4818885 - r4818889;
        double r4818891 = 3.0;
        double r4818892 = r4818891 * r4818887;
        double r4818893 = r4818892 * r4818892;
        double r4818894 = r4818892 * r4818893;
        double r4818895 = r4818885 - r4818894;
        double r4818896 = sqrt(r4818895);
        double r4818897 = r4818890 * r4818896;
        double r4818898 = r4818884 * r4818897;
        double r4818899 = r4818887 * r4818887;
        double r4818900 = r4818887 + r4818899;
        double r4818901 = r4818893 + r4818892;
        double r4818902 = r4818901 + r4818885;
        double r4818903 = sqrt(r4818902);
        double r4818904 = r4818900 * r4818903;
        double r4818905 = r4818904 + r4818903;
        double r4818906 = r4818898 / r4818905;
        return r4818906;
}

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

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

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

  7. Applied frac-times0.0

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

  9. Simplified0.0

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

  10. Final simplification0.0

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

Reproduce

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