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

Average Error: 0.4 → 0.3

Time: 17.3s

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)}\]

↓

\[\frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{6} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{6}\right)} \cdot t} \cdot \sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 r313654 = 1.0;
        double r313655 = 5.0;
        double r313656 = v;
        double r313657 = r313656 * r313656;
        double r313658 = r313655 * r313657;
        double r313659 = r313654 - r313658;
        double r313660 = atan2(1.0, 0.0);
        double r313661 = t;
        double r313662 = r313660 * r313661;
        double r313663 = 2.0;
        double r313664 = 3.0;
        double r313665 = r313664 * r313657;
        double r313666 = r313654 - r313665;
        double r313667 = r313663 * r313666;
        double r313668 = sqrt(r313667);
        double r313669 = r313662 * r313668;
        double r313670 = r313654 - r313657;
        double r313671 = r313669 * r313670;
        double r313672 = r313659 / r313671;
        return r313672;
}

↓

double f(double v, double t) {
        double r313673 = 1.0;
        double r313674 = 5.0;
        double r313675 = v;
        double r313676 = r313675 * r313675;
        double r313677 = r313674 * r313676;
        double r313678 = r313673 - r313677;
        double r313679 = atan2(1.0, 0.0);
        double r313680 = r313678 / r313679;
        double r313681 = 2.0;
        double r313682 = 6.0;
        double r313683 = pow(r313673, r313682);
        double r313684 = 3.0;
        double r313685 = r313684 * r313676;
        double r313686 = pow(r313685, r313682);
        double r313687 = r313683 - r313686;
        double r313688 = r313681 * r313687;
        double r313689 = sqrt(r313688);
        double r313690 = t;
        double r313691 = r313689 * r313690;
        double r313692 = r313680 / r313691;
        double r313693 = 3.0;
        double r313694 = pow(r313673, r313693);
        double r313695 = pow(r313685, r313693);
        double r313696 = r313694 + r313695;
        double r313697 = sqrt(r313696);
        double r313698 = r313692 * r313697;
        double r313699 = pow(r313675, r313682);
        double r313700 = r313694 - r313699;
        double r313701 = r313698 / r313700;
        double r313702 = r313673 * r313673;
        double r313703 = r313685 * r313685;
        double r313704 = r313673 * r313685;
        double r313705 = r313703 + r313704;
        double r313706 = r313702 + r313705;
        double r313707 = sqrt(r313706);
        double r313708 = r313676 * r313676;
        double r313709 = r313673 * r313676;
        double r313710 = r313708 + r313709;
        double r313711 = r313702 + r313710;
        double r313712 = r313707 * r313711;
        double r313713 = r313701 * r313712;
        return r313713;
}

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 flip3-- 0.4

   \[\leadsto \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 \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)}}}\]

4. Applied flip3-- 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\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)}}\]

5. 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\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)}}\]

6. 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\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.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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(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 frac-times 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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)}}}\]

9. 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}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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)}\]

10. Simplified 0.4

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

12. Applied associate-/r* 0.4

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

14. Applied flip-- 0.4

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

15. Applied associate-*r/ 0.4

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

    \[\leadsto \frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi \cdot t}}{\color{blue}{\frac{\sqrt{2 \cdot \left({1}^{3} \cdot {1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3} \cdot {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}\right)}}{\sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 associate-/r/ 0.4

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

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

20. Applied div-inv 0.4

    \[\leadsto \frac{\frac{\color{blue}{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi} \cdot \frac{1}{t}}}{\sqrt{2 \cdot \left({1}^{6} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{6}\right)}} \cdot \sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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-/l* 0.4

    \[\leadsto \frac{\color{blue}{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\frac{\sqrt{2 \cdot \left({1}^{6} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{6}\right)}}{\frac{1}{t}}}} \cdot \sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 \frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\color{blue}{\sqrt{2 \cdot \left({1}^{6} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{6}\right)} \cdot t}} \cdot \sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 \frac{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi}}{\sqrt{2 \cdot \left({1}^{6} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{6}\right)} \cdot t} \cdot \sqrt{{1}^{3} + {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}}{{1}^{3} - {v}^{6}} \cdot \left(\sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\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 2019350 +o rules:numerics
(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)))))