Average Error: 0.4 → 0.1
Time: 26.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)}\]
↓
\[\left(\frac{\frac{\frac{1}{\pi}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)} \cdot \left(1 \cdot \left(1 \cdot 1\right) - \left(\left(v \cdot v\right) \cdot v\right) \cdot \left(\left(v \cdot v\right) \cdot v\right)\right)}}{t} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(1 \cdot \left(v \cdot v\right) + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right)\right)\right) \cdot \left(1 - 5 \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)}
↓
\left(\frac{\frac{\frac{1}{\pi}}{\sqrt{2 \cdot \left(1 \cdot 1 - \left(\left(3 \cdot v\right) \cdot v\right) \cdot \left(\left(3 \cdot v\right) \cdot v\right)\right)} \cdot \left(1 \cdot \left(1 \cdot 1\right) - \left(\left(v \cdot v\right) \cdot v\right) \cdot \left(\left(v \cdot v\right) \cdot v\right)\right)}}{t} \cdot \left(\sqrt{1 + 3 \cdot \left(v \cdot v\right)} \cdot \left(1 \cdot 1 + \left(1 \cdot \left(v \cdot v\right) + \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right)\right)\right) \cdot \left(1 - 5 \cdot \left(v \cdot v\right)\right)
double f(double v, double t) {
        double r8073936 = 1.0;
        double r8073937 = 5.0;
        double r8073938 = v;
        double r8073939 = r8073938 * r8073938;
        double r8073940 = r8073937 * r8073939;
        double r8073941 = r8073936 - r8073940;
        double r8073942 = atan2(1.0, 0.0);
        double r8073943 = t;
        double r8073944 = r8073942 * r8073943;
        double r8073945 = 2.0;
        double r8073946 = 3.0;
        double r8073947 = r8073946 * r8073939;
        double r8073948 = r8073936 - r8073947;
        double r8073949 = r8073945 * r8073948;
        double r8073950 = sqrt(r8073949);
        double r8073951 = r8073944 * r8073950;
        double r8073952 = r8073936 - r8073939;
        double r8073953 = r8073951 * r8073952;
        double r8073954 = r8073941 / r8073953;
        return r8073954;
}
↓
double f(double v, double t) {
        double r8073955 = 1.0;
        double r8073956 = atan2(1.0, 0.0);
        double r8073957 = r8073955 / r8073956;
        double r8073958 = 2.0;
        double r8073959 = 1.0;
        double r8073960 = r8073959 * r8073959;
        double r8073961 = 3.0;
        double r8073962 = v;
        double r8073963 = r8073961 * r8073962;
        double r8073964 = r8073963 * r8073962;
        double r8073965 = r8073964 * r8073964;
        double r8073966 = r8073960 - r8073965;
        double r8073967 = r8073958 * r8073966;
        double r8073968 = sqrt(r8073967);
        double r8073969 = r8073959 * r8073960;
        double r8073970 = r8073962 * r8073962;
        double r8073971 = r8073970 * r8073962;
        double r8073972 = r8073971 * r8073971;
        double r8073973 = r8073969 - r8073972;
        double r8073974 = r8073968 * r8073973;
        double r8073975 = r8073957 / r8073974;
        double r8073976 = t;
        double r8073977 = r8073975 / r8073976;
        double r8073978 = r8073961 * r8073970;
        double r8073979 = r8073959 + r8073978;
        double r8073980 = sqrt(r8073979);
        double r8073981 = r8073959 * r8073970;
        double r8073982 = r8073970 * r8073970;
        double r8073983 = r8073981 + r8073982;
        double r8073984 = r8073960 + r8073983;
        double r8073985 = r8073980 * r8073984;
        double r8073986 = r8073977 * r8073985;
        double r8073987 = 5.0;
        double r8073988 = r8073987 * r8073970;
        double r8073989 = r8073959 - r8073988;
        double r8073990 = r8073986 * r8073989;
        return r8073990;
}

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 associate-/l*0.4

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

  6. Applied div-inv0.4

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

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

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

  8. Applied sqrt-prod0.4

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

  9. Applied times-frac0.4

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

  10. Simplified0.4

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

  11. Simplified0.4

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

  13. Applied associate-/r*0.3

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

  15. Applied flip3--0.3

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

  16. Applied flip--0.3

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

  17. Applied associate-*r/0.3

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

  18. Applied sqrt-div0.3

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

  19. Applied frac-times0.3

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

  20. Applied associate-/r/0.3

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

  21. Simplified0.1

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

  22. Final simplification0.1

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

Reproduce

herbie shell --seed 2019172 +o rules:numerics
(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)))))