Falkner and Boettcher, Appendix B, 1

Average Error: 0.6 → 0.6

Time: 6.2s

Precision: 64

Math

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

↓

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

C

double f(double v) {
        double r272187 = 1.0;
        double r272188 = 5.0;
        double r272189 = v;
        double r272190 = r272189 * r272189;
        double r272191 = r272188 * r272190;
        double r272192 = r272187 - r272191;
        double r272193 = r272190 - r272187;
        double r272194 = r272192 / r272193;
        double r272195 = acos(r272194);
        return r272195;
}

↓

double f(double v) {
        double r272196 = 1.0;
        double r272197 = 5.0;
        double r272198 = v;
        double r272199 = r272198 * r272198;
        double r272200 = r272197 * r272199;
        double r272201 = r272196 - r272200;
        double r272202 = r272199 - r272196;
        double r272203 = r272201 / r272202;
        double r272204 = asin(r272203);
        double r272205 = atan2(1.0, 0.0);
        double r272206 = 2.0;
        double r272207 = r272205 / r272206;
        double r272208 = r272204 + r272207;
        double r272209 = r272204 * r272208;
        double r272210 = r272207 * r272207;
        double r272211 = r272209 + r272210;
        double r272212 = cbrt(r272211);
        double r272213 = r272211 / r272212;
        double r272214 = r272213 / r272212;
        double r272215 = r272207 - r272204;
        double r272216 = r272215 / r272212;
        double r272217 = r272214 * r272216;
        return r272217;
}

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 *-un-lft-identity 0.6

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

5. Applied acos-asin 0.6

   \[\leadsto 1 \cdot \color{blue}{\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 flip3-- 0.6

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

8. Simplified 0.6

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

10. Applied add-cube-cbrt 1.5

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

11. Applied difference-cubes 1.5

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

12. Applied times-frac 1.5

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

13. Simplified 0.6

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

14. Final simplification 0.6

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

Reproduce

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