Average Error: 0.5 → 0.3
Time: 11.7s
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(\left(\frac{\frac{1}{\pi}}{\sqrt{2 \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right)} \cdot \mathsf{fma}\left(1 \cdot 1, 1, {v}^{6}\right)} \cdot \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{t}}{{1}^{3} - {\left(v \cdot v\right)}^{3}}\right) \cdot \left(\sqrt{1 \cdot 1 + \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\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)\]
\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(\left(\frac{\frac{1}{\pi}}{\sqrt{2 \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right)} \cdot \mathsf{fma}\left(1 \cdot 1, 1, {v}^{6}\right)} \cdot \frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{t}}{{1}^{3} - {\left(v \cdot v\right)}^{3}}\right) \cdot \left(\sqrt{1 \cdot 1 + \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\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)
double f(double v, double t) {
        double r294993 = 1.0;
        double r294994 = 5.0;
        double r294995 = v;
        double r294996 = r294995 * r294995;
        double r294997 = r294994 * r294996;
        double r294998 = r294993 - r294997;
        double r294999 = atan2(1.0, 0.0);
        double r295000 = t;
        double r295001 = r294999 * r295000;
        double r295002 = 2.0;
        double r295003 = 3.0;
        double r295004 = r295003 * r294996;
        double r295005 = r294993 - r295004;
        double r295006 = r295002 * r295005;
        double r295007 = sqrt(r295006);
        double r295008 = r295001 * r295007;
        double r295009 = r294993 - r294996;
        double r295010 = r295008 * r295009;
        double r295011 = r294998 / r295010;
        return r295011;
}

double f(double v, double t) {
        double r295012 = 1.0;
        double r295013 = atan2(1.0, 0.0);
        double r295014 = r295012 / r295013;
        double r295015 = 2.0;
        double r295016 = 1.0;
        double r295017 = r295016 * r295016;
        double r295018 = r295017 * r295017;
        double r295019 = 3.0;
        double r295020 = v;
        double r295021 = r295020 * r295020;
        double r295022 = r295019 * r295021;
        double r295023 = r295022 * r295022;
        double r295024 = r295023 * r295023;
        double r295025 = r295018 - r295024;
        double r295026 = r295015 * r295025;
        double r295027 = sqrt(r295026);
        double r295028 = 6.0;
        double r295029 = pow(r295020, r295028);
        double r295030 = fma(r295017, r295016, r295029);
        double r295031 = r295027 * r295030;
        double r295032 = r295014 / r295031;
        double r295033 = 5.0;
        double r295034 = r295033 * r295021;
        double r295035 = r295016 - r295034;
        double r295036 = t;
        double r295037 = r295035 / r295036;
        double r295038 = 3.0;
        double r295039 = pow(r295016, r295038);
        double r295040 = pow(r295021, r295038);
        double r295041 = r295039 - r295040;
        double r295042 = r295037 / r295041;
        double r295043 = r295032 * r295042;
        double r295044 = r295017 + r295023;
        double r295045 = sqrt(r295044);
        double r295046 = r295039 + r295040;
        double r295047 = r295045 * r295046;
        double r295048 = r295043 * r295047;
        double r295049 = r295016 + r295022;
        double r295050 = sqrt(r295049);
        double r295051 = r295021 * r295021;
        double r295052 = r295016 * r295021;
        double r295053 = r295051 + r295052;
        double r295054 = r295017 + r295053;
        double r295055 = r295050 * r295054;
        double r295056 = r295048 * r295055;
        return r295056;
}

Error

Bits error versus v

Bits error versus t

Derivation

  1. Initial program 0.5

    \[\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.5

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

    \[\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 \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.5

    \[\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 \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-div0.5

    \[\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 \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.5

    \[\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 \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-times0.5

    \[\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}^{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)}}}\]
  9. Applied associate-/r/0.5

    \[\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}^{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)}\]
  10. Using strategy rm
  11. Applied flip--0.5

    \[\leadsto \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 \color{blue}{\frac{{1}^{3} \cdot {1}^{3} - {\left(v \cdot v\right)}^{3} \cdot {\left(v \cdot v\right)}^{3}}{{1}^{3} + {\left(v \cdot v\right)}^{3}}}} \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)\]
  12. Applied flip--0.5

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

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

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

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

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

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

    \[\leadsto \left(\color{blue}{\frac{\frac{1 - 5 \cdot \left(v \cdot v\right)}{\pi \cdot t}}{\left(\sqrt{2 \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right)} \cdot \mathsf{fma}\left(1 \cdot 1, 1, {v}^{6}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}} \cdot \left(\sqrt{1 \cdot 1 + \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\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)\]
  19. Using strategy rm
  20. Applied *-un-lft-identity0.5

    \[\leadsto \left(\frac{\frac{\color{blue}{1 \cdot \left(1 - 5 \cdot \left(v \cdot v\right)\right)}}{\pi \cdot t}}{\left(\sqrt{2 \cdot \left(\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)\right)} \cdot \mathsf{fma}\left(1 \cdot 1, 1, {v}^{6}\right)\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)} \cdot \left(\sqrt{1 \cdot 1 + \left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right)} \cdot \left({1}^{3} + {\left(v \cdot v\right)}^{3}\right)\right)\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)\]
  21. Applied times-frac0.4

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

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

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

Reproduce

herbie shell --seed 2019346 +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)))))