Average Error: 0.6 → 0.6
Time: 41.4s
Precision: 64
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\]
↓
\[{\left(e^{\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \left(v \cdot v\right) \cdot 5}{v \cdot v - 1}\right)\right)}}\right)}^{\left(\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \log \left(e^{\left(v \cdot v\right) \cdot 5}\right)}{v \cdot v - 1}\right)\right)}\right)}\]
\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
↓
{\left(e^{\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \left(v \cdot v\right) \cdot 5}{v \cdot v - 1}\right)\right)}}\right)}^{\left(\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \log \left(e^{\left(v \cdot v\right) \cdot 5}\right)}{v \cdot v - 1}\right)\right)}\right)}
double f(double v) {
        double r45471977 = 1.0;
        double r45471978 = 5.0;
        double r45471979 = v;
        double r45471980 = r45471979 * r45471979;
        double r45471981 = r45471978 * r45471980;
        double r45471982 = r45471977 - r45471981;
        double r45471983 = r45471980 - r45471977;
        double r45471984 = r45471982 / r45471983;
        double r45471985 = acos(r45471984);
        return r45471985;
}
↓
double f(double v) {
        double r45471986 = atan2(1.0, 0.0);
        double r45471987 = 2.0;
        double r45471988 = r45471986 / r45471987;
        double r45471989 = 1.0;
        double r45471990 = v;
        double r45471991 = r45471990 * r45471990;
        double r45471992 = 5.0;
        double r45471993 = r45471991 * r45471992;
        double r45471994 = r45471989 - r45471993;
        double r45471995 = r45471991 - r45471989;
        double r45471996 = r45471994 / r45471995;
        double r45471997 = asin(r45471996);
        double r45471998 = r45471988 - r45471997;
        double r45471999 = log(r45471998);
        double r45472000 = sqrt(r45471999);
        double r45472001 = exp(r45472000);
        double r45472002 = exp(r45471993);
        double r45472003 = log(r45472002);
        double r45472004 = r45471989 - r45472003;
        double r45472005 = r45472004 / r45471995;
        double r45472006 = asin(r45472005);
        double r45472007 = r45471988 - r45472006;
        double r45472008 = log(r45472007);
        double r45472009 = sqrt(r45472008);
        double r45472010 = pow(r45472001, r45472009);
        return r45472010;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

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. Using strategy rm

  5. Applied add-exp-log0.6

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

    \[\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. Applied exp-prod0.6

    \[\leadsto \color{blue}{{\left(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)}}\right)}^{\left(\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)}\right)}}\]
  9. Using strategy rm

  10. Applied add-log-exp0.6

    \[\leadsto {\left(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)}}\right)}^{\left(\sqrt{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\frac{1 - \color{blue}{\log \left(e^{5 \cdot \left(v \cdot v\right)}\right)}}{v \cdot v - 1}\right)\right)}\right)}\]

  11. Final simplification0.6

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

Reproduce

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