Average Error: 0.0 → 0.0
Time: 15.1s
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(\frac{\sqrt{2}}{4} \cdot \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 \left(1 - v \cdot v\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(\frac{\sqrt{2}}{4} \cdot \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 \left(1 - v \cdot v\right)
double f(double v) {
        double r141188 = 2.0;
        double r141189 = sqrt(r141188);
        double r141190 = 4.0;
        double r141191 = r141189 / r141190;
        double r141192 = 1.0;
        double r141193 = 3.0;
        double r141194 = v;
        double r141195 = r141194 * r141194;
        double r141196 = r141193 * r141195;
        double r141197 = r141192 - r141196;
        double r141198 = sqrt(r141197);
        double r141199 = r141191 * r141198;
        double r141200 = r141192 - r141195;
        double r141201 = r141199 * r141200;
        return r141201;
}
↓
double f(double v) {
        double r141202 = 2.0;
        double r141203 = sqrt(r141202);
        double r141204 = 4.0;
        double r141205 = r141203 / r141204;
        double r141206 = 1.0;
        double r141207 = 3.0;
        double r141208 = pow(r141206, r141207);
        double r141209 = 3.0;
        double r141210 = v;
        double r141211 = r141210 * r141210;
        double r141212 = r141209 * r141211;
        double r141213 = pow(r141212, r141207);
        double r141214 = r141208 - r141213;
        double r141215 = sqrt(r141214);
        double r141216 = r141206 * r141206;
        double r141217 = r141212 * r141212;
        double r141218 = r141206 * r141212;
        double r141219 = r141217 + r141218;
        double r141220 = r141216 + r141219;
        double r141221 = sqrt(r141220);
        double r141222 = r141215 / r141221;
        double r141223 = r141205 * r141222;
        double r141224 = r141206 - r141211;
        double r141225 = r141223 * r141224;
        return r141225;
}

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{\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 \left(1 - v \cdot v\right)\]

  4. 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 \left(1 - v \cdot v\right)\]

  5. Final simplification0.0

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

Reproduce

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