Average Error: 0.5 → 0.5
Time: 6.8s
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}{{v}^{2} - 1} - \frac{5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
\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}{{v}^{2} - 1} - \frac{5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
double f(double v) {
        double r234604 = 1.0;
        double r234605 = 5.0;
        double r234606 = v;
        double r234607 = r234606 * r234606;
        double r234608 = r234605 * r234607;
        double r234609 = r234604 - r234608;
        double r234610 = r234607 - r234604;
        double r234611 = r234609 / r234610;
        double r234612 = acos(r234611);
        return r234612;
}
↓
double f(double v) {
        double r234613 = atan2(1.0, 0.0);
        double r234614 = 2.0;
        double r234615 = r234613 / r234614;
        double r234616 = 1.0;
        double r234617 = v;
        double r234618 = pow(r234617, r234614);
        double r234619 = r234618 - r234616;
        double r234620 = r234616 / r234619;
        double r234621 = 5.0;
        double r234622 = r234617 * r234617;
        double r234623 = r234621 * r234622;
        double r234624 = r234622 - r234616;
        double r234625 = r234623 / r234624;
        double r234626 = r234620 - r234625;
        double r234627 = asin(r234626);
        double r234628 = r234615 - r234627;
        return r234628;
}

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 div-sub0.5

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

  4. Simplified0.5

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

  6. Applied acos-asin0.5

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

  7. Final simplification0.5

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

Reproduce

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