Average Error: 0.0 → 0.0
Time: 6.5s
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} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{\left(4 \cdot \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)
↓
\frac{\left(\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{\left(4 \cdot \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 r333550 = 2.0;
        double r333551 = sqrt(r333550);
        double r333552 = 4.0;
        double r333553 = r333551 / r333552;
        double r333554 = 1.0;
        double r333555 = 3.0;
        double r333556 = v;
        double r333557 = r333556 * r333556;
        double r333558 = r333555 * r333557;
        double r333559 = r333554 - r333558;
        double r333560 = sqrt(r333559);
        double r333561 = r333553 * r333560;
        double r333562 = r333554 - r333557;
        double r333563 = r333561 * r333562;
        return r333563;
}
↓
double f(double v) {
        double r333564 = 2.0;
        double r333565 = sqrt(r333564);
        double r333566 = 1.0;
        double r333567 = 3.0;
        double r333568 = pow(r333566, r333567);
        double r333569 = 3.0;
        double r333570 = v;
        double r333571 = r333570 * r333570;
        double r333572 = r333569 * r333571;
        double r333573 = pow(r333572, r333567);
        double r333574 = r333568 - r333573;
        double r333575 = sqrt(r333574);
        double r333576 = r333565 * r333575;
        double r333577 = r333566 * r333566;
        double r333578 = r333571 * r333571;
        double r333579 = r333577 - r333578;
        double r333580 = r333576 * r333579;
        double r333581 = 4.0;
        double r333582 = r333572 * r333572;
        double r333583 = r333566 * r333572;
        double r333584 = r333582 + r333583;
        double r333585 = r333577 + r333584;
        double r333586 = sqrt(r333585);
        double r333587 = r333581 * r333586;
        double r333588 = r333566 + r333571;
        double r333589 = r333587 * r333588;
        double r333590 = r333580 / r333589;
        return r333590;
}

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

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

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

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

  6. Applied frac-times0.0

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

  7. Applied frac-times0.0

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

  8. Final simplification0.0

    \[\leadsto \frac{\left(\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{\left(4 \cdot \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 2020036 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))