Average Error: 0.5 → 0.5
Time: 13.9s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[e^{\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)} \cdot \sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)}}\]
\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
e^{\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)} \cdot \sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)}}
double f(double v) {
        double r138358 = 1.0;
        double r138359 = 5.0;
        double r138360 = v;
        double r138361 = r138360 * r138360;
        double r138362 = r138359 * r138361;
        double r138363 = r138358 - r138362;
        double r138364 = r138361 - r138358;
        double r138365 = r138363 / r138364;
        double r138366 = acos(r138365);
        return r138366;
}
↓
double f(double v) {
        double r138367 = atan2(1.0, 0.0);
        double r138368 = 2.0;
        double r138369 = r138367 / r138368;
        double r138370 = 1.0;
        double r138371 = 5.0;
        double r138372 = v;
        double r138373 = r138372 * r138372;
        double r138374 = r138371 * r138373;
        double r138375 = r138370 - r138374;
        double r138376 = r138373 - r138370;
        double r138377 = r138375 / r138376;
        double r138378 = asin(r138377);
        double r138379 = r138369 - r138378;
        double r138380 = log(r138379);
        double r138381 = sqrt(r138380);
        double r138382 = r138381 * r138381;
        double r138383 = exp(r138382);
        return r138383;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.5

    \[\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.5

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

  5. Applied add-exp-log0.5

    \[\leadsto \color{blue}{e^{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)}}\]
  6. Using strategy rm

  7. Applied add-sqr-sqrt0.5

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

  8. Final simplification0.5

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

Reproduce

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