Average Error: 0.6 → 0.6
Time: 38.9s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \left(v \cdot v\right) \cdot 5}{v \cdot v - 1}\right)\]
double f(double v) {
        double r42175170 = 1.0;
        double r42175171 = 5.0;
        double r42175172 = v;
        double r42175173 = r42175172 * r42175172;
        double r42175174 = r42175171 * r42175173;
        double r42175175 = r42175170 - r42175174;
        double r42175176 = r42175173 - r42175170;
        double r42175177 = r42175175 / r42175176;
        double r42175178 = acos(r42175177);
        return r42175178;
}
↓
double f(double v) {
        double r42175179 = atan2(1.0, 0.0);
        double r42175180 = 2.0;
        double r42175181 = r42175179 / r42175180;
        double r42175182 = 1.0;
        double r42175183 = v;
        double r42175184 = r42175183 * r42175183;
        double r42175185 = 5.0;
        double r42175186 = r42175184 * r42175185;
        double r42175187 = r42175182 - r42175186;
        double r42175188 = r42175184 - r42175182;
        double r42175189 = r42175187 / r42175188;
        double r42175190 = asin(r42175189);
        double r42175191 = r42175181 - r42175190;
        return r42175191;
}


\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \left(v \cdot v\right) \cdot 5}{v \cdot v - 1}\right)

Error

Bits error versus v

Derivation

  1. Initial program 0.6

    \[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
  2. Using strategy rm

  3. Applied acos-asin0.6

    \[\leadsto \color{blue}{\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)}\]

  4. Final simplification0.6

    \[\leadsto \frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \left(v \cdot v\right) \cdot 5}{v \cdot v - 1}\right)\]

Reproduce

herbie shell --seed 2019101 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 1"
  (acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))