Average Error: 0.0 → 0.0
Time: 17.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{\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{4 \cdot \sqrt{\mathsf{fma}\left(3 \cdot \left(v \cdot v\right), \mathsf{fma}\left(3, v \cdot v, 1\right), 1 \cdot 1\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{\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{4 \cdot \sqrt{\mathsf{fma}\left(3 \cdot \left(v \cdot v\right), \mathsf{fma}\left(3, v \cdot v, 1\right), 1 \cdot 1\right)}} \cdot \left(1 - v \cdot v\right)
double f(double v) {
        double r193745 = 2.0;
        double r193746 = sqrt(r193745);
        double r193747 = 4.0;
        double r193748 = r193746 / r193747;
        double r193749 = 1.0;
        double r193750 = 3.0;
        double r193751 = v;
        double r193752 = r193751 * r193751;
        double r193753 = r193750 * r193752;
        double r193754 = r193749 - r193753;
        double r193755 = sqrt(r193754);
        double r193756 = r193748 * r193755;
        double r193757 = r193749 - r193752;
        double r193758 = r193756 * r193757;
        return r193758;
}
↓
double f(double v) {
        double r193759 = 2.0;
        double r193760 = sqrt(r193759);
        double r193761 = 1.0;
        double r193762 = 3.0;
        double r193763 = pow(r193761, r193762);
        double r193764 = 3.0;
        double r193765 = v;
        double r193766 = r193765 * r193765;
        double r193767 = r193764 * r193766;
        double r193768 = pow(r193767, r193762);
        double r193769 = r193763 - r193768;
        double r193770 = sqrt(r193769);
        double r193771 = r193760 * r193770;
        double r193772 = 4.0;
        double r193773 = fma(r193764, r193766, r193761);
        double r193774 = r193761 * r193761;
        double r193775 = fma(r193767, r193773, r193774);
        double r193776 = sqrt(r193775);
        double r193777 = r193772 * r193776;
        double r193778 = r193771 / r193777;
        double r193779 = r193761 - r193766;
        double r193780 = r193778 * r193779;
        return r193780;
}

Error

Bits error versus v

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

  6. Simplified0.0

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

  7. Final simplification0.0

    \[\leadsto \frac{\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{4 \cdot \sqrt{\mathsf{fma}\left(3 \cdot \left(v \cdot v\right), \mathsf{fma}\left(3, v \cdot v, 1\right), 1 \cdot 1\right)}} \cdot \left(1 - v \cdot v\right)\]

Reproduce

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