Average Error: 0.4 → 0.1
Time: 40.6s
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 r7857820 = 1.0;
        double r7857821 = 5.0;
        double r7857822 = v;
        double r7857823 = r7857822 * r7857822;
        double r7857824 = r7857821 * r7857823;
        double r7857825 = r7857820 - r7857824;
        double r7857826 = atan2(1.0, 0.0);
        double r7857827 = t;
        double r7857828 = r7857826 * r7857827;
        double r7857829 = 2.0;
        double r7857830 = 3.0;
        double r7857831 = r7857830 * r7857823;
        double r7857832 = r7857820 - r7857831;
        double r7857833 = r7857829 * r7857832;
        double r7857834 = sqrt(r7857833);
        double r7857835 = r7857828 * r7857834;
        double r7857836 = r7857820 - r7857823;
        double r7857837 = r7857835 * r7857836;
        double r7857838 = r7857825 / r7857837;
        return r7857838;
}
↓
double f(double v, double t) {
        double r7857839 = 1.0;
        double r7857840 = v;
        double r7857841 = r7857840 * r7857840;
        double r7857842 = 5.0;
        double r7857843 = r7857841 * r7857842;
        double r7857844 = r7857839 - r7857843;
        double r7857845 = sqrt(r7857844);
        double r7857846 = r7857839 - r7857841;
        double r7857847 = r7857845 / r7857846;
        double r7857848 = 3.0;
        double r7857849 = r7857848 * r7857841;
        double r7857850 = r7857839 + r7857849;
        double r7857851 = 2.0;
        double r7857852 = r7857839 - r7857849;
        double r7857853 = r7857851 * r7857852;
        double r7857854 = r7857850 * r7857853;
        double r7857855 = sqrt(r7857854);
        double r7857856 = r7857845 / r7857855;
        double r7857857 = atan2(1.0, 0.0);
        double r7857858 = r7857856 / r7857857;
        double r7857859 = t;
        double r7857860 = r7857858 / r7857859;
        double r7857861 = sqrt(r7857850);
        double r7857862 = r7857860 * r7857861;
        double r7857863 = r7857847 * r7857862;
        return r7857863;
}

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)))))