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

Average Error: 0.4 → 0.1

Time: 18.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)}{1 - v \cdot v}}{\pi}}{\sqrt{2 \cdot \left({1}^{4} - {v}^{8} \cdot {3}^{4}\right)}}}{t} \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right) \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

C

double f(double v, double t) {
        double r293173 = 1.0;
        double r293174 = 5.0;
        double r293175 = v;
        double r293176 = r293175 * r293175;
        double r293177 = r293174 * r293176;
        double r293178 = r293173 - r293177;
        double r293179 = atan2(1.0, 0.0);
        double r293180 = t;
        double r293181 = r293179 * r293180;
        double r293182 = 2.0;
        double r293183 = 3.0;
        double r293184 = r293183 * r293176;
        double r293185 = r293173 - r293184;
        double r293186 = r293182 * r293185;
        double r293187 = sqrt(r293186);
        double r293188 = r293181 * r293187;
        double r293189 = r293173 - r293176;
        double r293190 = r293188 * r293189;
        double r293191 = r293178 / r293190;
        return r293191;
}

↓

double f(double v, double t) {
        double r293192 = 1.0;
        double r293193 = 5.0;
        double r293194 = v;
        double r293195 = r293194 * r293194;
        double r293196 = r293193 * r293195;
        double r293197 = r293192 - r293196;
        double r293198 = r293192 - r293195;
        double r293199 = r293197 / r293198;
        double r293200 = atan2(1.0, 0.0);
        double r293201 = r293199 / r293200;
        double r293202 = 2.0;
        double r293203 = 4.0;
        double r293204 = pow(r293192, r293203);
        double r293205 = 8.0;
        double r293206 = pow(r293194, r293205);
        double r293207 = 3.0;
        double r293208 = pow(r293207, r293203);
        double r293209 = r293206 * r293208;
        double r293210 = r293204 - r293209;
        double r293211 = r293202 * r293210;
        double r293212 = sqrt(r293211);
        double r293213 = r293201 / r293212;
        double r293214 = t;
        double r293215 = r293213 / r293214;
        double r293216 = r293192 * r293192;
        double r293217 = r293207 * r293207;
        double r293218 = pow(r293194, r293203);
        double r293219 = r293217 * r293218;
        double r293220 = r293216 + r293219;
        double r293221 = sqrt(r293220);
        double r293222 = r293215 * r293221;
        double r293223 = r293207 * r293195;
        double r293224 = r293192 + r293223;
        double r293225 = sqrt(r293224);
        double r293226 = r293222 * r293225;
        return r293226;
}

Error

Bits error versus v

Bits error versus t

Derivation

1. Initial program 0.4

   \[\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 flip-- 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \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) \cdot \left(1 - v \cdot v\right)}\]

4. Applied associate-*r/ 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \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) \cdot \left(1 - v \cdot v\right)}\]

5. Applied sqrt-div 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \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) \cdot \left(1 - v \cdot v\right)}\]

6. Applied associate-*r/ 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\pi \cdot t\right) \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)}}} \cdot \left(1 - v \cdot v\right)}\]

7. Applied associate-*l/ 0.4

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(\left(\pi \cdot t\right) \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) \cdot \left(1 - v \cdot v\right)}{\sqrt{1 + 3 \cdot \left(v \cdot v\right)}}}}\]

8. Applied associate-/r/ 0.4

   \[\leadsto \color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \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) \cdot \left(1 - v \cdot v\right)} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}}\]

9. Simplified 0.4

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

11. Applied flip-- 0.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)\right)} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

12. Applied associate-*l/ 0.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)\right)} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

13. Applied sqrt-div 0.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)\right)} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

14. Applied associate-*l/ 0.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)}{\sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}}} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

15. Applied associate-*r/ 0.4

    \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\frac{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)\right)}{\sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}}}} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

16. Applied associate-/r/ 0.4

    \[\leadsto \color{blue}{\left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(1 - v \cdot v\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 \left(\pi \cdot t\right)\right)} \cdot \sqrt{1 \cdot 1 + \left(3 \cdot 3\right) \cdot {v}^{4}}\right)} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\]

17. Simplified 0.4

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

19. Applied *-un-lft-identity 0.4

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

20. Applied *-un-lft-identity 0.4

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

21. Applied *-un-lft-identity 0.4

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

22. Applied times-frac 0.4

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

23. Applied times-frac 0.4

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

24. Applied times-frac 0.3

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

25. Simplified 0.3

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

26. Simplified 0.3

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

28. Applied associate-*l/ 0.1

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

29. Simplified 0.1

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

30. Final simplification 0.1

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

Reproduce

herbie shell --seed 2019351 
(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)))))