Average Error: 0.4 → 0.1
Time: 39.9s
Precision: 64
\[\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{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v} \cdot \left(\frac{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\sqrt{\left(1 + 3 \cdot \left(v \cdot v\right)\right) \cdot \left(2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)\right)}}}{\pi}}{t} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\right)\]
\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{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v} \cdot \left(\frac{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\sqrt{\left(1 + 3 \cdot \left(v \cdot v\right)\right) \cdot \left(2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)\right)}}}{\pi}}{t} \cdot \sqrt{1 + 3 \cdot \left(v \cdot v\right)}\right)
double f(double v, double t) {
        double r7857779 = 1.0;
        double r7857780 = 5.0;
        double r7857781 = v;
        double r7857782 = r7857781 * r7857781;
        double r7857783 = r7857780 * r7857782;
        double r7857784 = r7857779 - r7857783;
        double r7857785 = atan2(1.0, 0.0);
        double r7857786 = t;
        double r7857787 = r7857785 * r7857786;
        double r7857788 = 2.0;
        double r7857789 = 3.0;
        double r7857790 = r7857789 * r7857782;
        double r7857791 = r7857779 - r7857790;
        double r7857792 = r7857788 * r7857791;
        double r7857793 = sqrt(r7857792);
        double r7857794 = r7857787 * r7857793;
        double r7857795 = r7857779 - r7857782;
        double r7857796 = r7857794 * r7857795;
        double r7857797 = r7857784 / r7857796;
        return r7857797;
}
↓
double f(double v, double t) {
        double r7857798 = 1.0;
        double r7857799 = v;
        double r7857800 = r7857799 * r7857799;
        double r7857801 = 5.0;
        double r7857802 = r7857800 * r7857801;
        double r7857803 = r7857798 - r7857802;
        double r7857804 = sqrt(r7857803);
        double r7857805 = r7857798 - r7857800;
        double r7857806 = r7857804 / r7857805;
        double r7857807 = 3.0;
        double r7857808 = r7857807 * r7857800;
        double r7857809 = r7857798 + r7857808;
        double r7857810 = 2.0;
        double r7857811 = r7857798 - r7857808;
        double r7857812 = r7857810 * r7857811;
        double r7857813 = r7857809 * r7857812;
        double r7857814 = sqrt(r7857813);
        double r7857815 = r7857804 / r7857814;
        double r7857816 = atan2(1.0, 0.0);
        double r7857817 = r7857815 / r7857816;
        double r7857818 = t;
        double r7857819 = r7857817 / r7857818;
        double r7857820 = sqrt(r7857809);
        double r7857821 = r7857819 * r7857820;
        double r7857822 = r7857806 * r7857821;
        return r7857822;
}

Error

Bits error versus v

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

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 add-sqr-sqrt0.4

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

  4. Applied times-frac0.4

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

  6. Applied *-un-lft-identity0.4

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

  7. Applied sqrt-prod0.4

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

  8. Applied times-frac0.5

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

  9. Simplified0.5

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

  11. Applied flip--0.5

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

  12. Applied associate-*r/0.5

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

  13. Applied sqrt-div0.5

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

  14. Applied associate-/r/0.5

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

  15. Applied associate-*r*0.5

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

  16. Simplified0.1

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

  17. Final simplification0.1

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

Reproduce

herbie shell --seed 2019200 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  (/ (- 1.0 (* 5.0 (* v v))) (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))