Falkner and Boettcher, Equation (20:1,3)

Average Error: 0.5 → 0.3

Time: 14.1s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\left(\frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{{1}^{6} - {v}^{12}}}{t}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot \left(3 \cdot {3}^{3}\right)\right)}} \cdot \left(\left({1}^{3} + {v}^{6}\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right) \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

C

double f(double v, double t) {
        double r194203 = 1.0;
        double r194204 = 5.0;
        double r194205 = v;
        double r194206 = r194205 * r194205;
        double r194207 = r194204 * r194206;
        double r194208 = r194203 - r194207;
        double r194209 = atan2(1.0, 0.0);
        double r194210 = t;
        double r194211 = r194209 * r194210;
        double r194212 = 2.0;
        double r194213 = 3.0;
        double r194214 = r194213 * r194206;
        double r194215 = r194203 - r194214;
        double r194216 = r194212 * r194215;
        double r194217 = sqrt(r194216);
        double r194218 = r194211 * r194217;
        double r194219 = r194203 - r194206;
        double r194220 = r194218 * r194219;
        double r194221 = r194208 / r194220;
        return r194221;
}

↓

double f(double v, double t) {
        double r194222 = 1.0;
        double r194223 = 5.0;
        double r194224 = v;
        double r194225 = r194224 * r194224;
        double r194226 = r194223 * r194225;
        double r194227 = r194222 - r194226;
        double r194228 = atan2(1.0, 0.0);
        double r194229 = r194227 / r194228;
        double r194230 = 6.0;
        double r194231 = pow(r194222, r194230);
        double r194232 = 12.0;
        double r194233 = pow(r194224, r194232);
        double r194234 = r194231 - r194233;
        double r194235 = r194229 / r194234;
        double r194236 = t;
        double r194237 = r194235 / r194236;
        double r194238 = 2.0;
        double r194239 = 4.0;
        double r194240 = pow(r194222, r194239);
        double r194241 = 8.0;
        double r194242 = pow(r194224, r194241);
        double r194243 = 3.0;
        double r194244 = 3.0;
        double r194245 = pow(r194243, r194244);
        double r194246 = r194243 * r194245;
        double r194247 = r194242 * r194246;
        double r194248 = r194240 - r194247;
        double r194249 = r194238 * r194248;
        double r194250 = sqrt(r194249);
        double r194251 = r194237 / r194250;
        double r194252 = pow(r194222, r194244);
        double r194253 = pow(r194224, r194230);
        double r194254 = r194252 + r194253;
        double r194255 = r194222 * r194222;
        double r194256 = r194243 * r194243;
        double r194257 = pow(r194224, r194239);
        double r194258 = r194256 * r194257;
        double r194259 = r194255 + r194258;
        double r194260 = sqrt(r194259);
        double r194261 = r194254 * r194260;
        double r194262 = r194251 * r194261;
        double r194263 = r194243 * r194225;
        double r194264 = r194222 + r194263;
        double r194265 = sqrt(r194264);
        double r194266 = r194225 * r194225;
        double r194267 = r194222 * r194225;
        double r194268 = r194266 + r194267;
        double r194269 = r194255 + r194268;
        double r194270 = r194265 * r194269;
        double r194271 = r194262 * r194270;
        return r194271;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.5

   \[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
2. Using strategy rm

3. Applied associate-*l* 0.5

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

5. Applied flip3-- 0.5

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

6. Applied flip-- 0.5

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

7. Applied associate-*r/ 0.5

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

8. Applied sqrt-div 0.5

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

9. Applied associate-*r/ 0.5

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

10. Applied associate-*r/ 0.5

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

11. Applied frac-times 0.5

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

12. Applied associate-/r/ 0.5

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

13. Simplified 0.3

    \[\leadsto \color{blue}{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\left({1}^{3} - {v}^{6}\right) \cdot \left(\sqrt{\left(1 \cdot 1 - \left(3 \cdot 3\right) \cdot {v}^{4}\right) \cdot 2} \cdot t\right)}} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]
14. Using strategy rm

15. Applied flip-- 0.3

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

16. Applied associate-*l/ 0.3

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

17. Applied sqrt-div 0.3

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

18. Applied associate-*l/ 0.3

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

19. Applied flip-- 0.3

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

20. Applied frac-times 0.3

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

21. Applied associate-/r/ 0.3

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

22. Simplified 0.3

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

23. Final simplification 0.3

    \[\leadsto \left(\frac{\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{{1}^{6} - {v}^{12}}}{t}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot \left(3 \cdot {3}^{3}\right)\right)}} \cdot \left(\left({1}^{3} + {v}^{6}\right) \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)\right) \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)\right)\]

Reproduce

herbie shell --seed 2020042 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  :precision binary64
  (/ (- 1 (* 5 (* v v))) (* (* (* PI t) (sqrt (* 2 (- 1 (* 3 (* v v)))))) (- 1 (* v v)))))