1 / 4 / PI / r^2 * a * (erf(r / t) - 2 / sqrt(PI) * exp(- r^2 / t^2) * r)

Percentage Accurate: 99.1% → 99.2%
Time: 8.2s
Alternatives: 9
Speedup: 2.0×

Specification

?
\[\left(\left(10^{-10} \leq r \land r \leq 10000000000\right) \land \left(0 \leq a \land a \leq 1\right)\right) \land \left(10^{-6} \leq t \land t \leq 1\right)\]
\[\begin{array}{l} \\ \left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \end{array} \]
(FPCore (r a t)
 :precision binary64
 (*
  (* (/ (/ (/ 1.0 4.0) (PI)) (pow r 2.0)) a)
  (-
   (erf (/ r t))
   (* (* (/ 2.0 (sqrt (PI))) (exp (/ (- (pow r 2.0)) (pow t 2.0)))) r))))
\begin{array}{l}

\\
\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right)
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 9 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 99.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \end{array} \]
(FPCore (r a t)
 :precision binary64
 (*
  (* (/ (/ (/ 1.0 4.0) (PI)) (pow r 2.0)) a)
  (-
   (erf (/ r t))
   (* (* (/ 2.0 (sqrt (PI))) (exp (/ (- (pow r 2.0)) (pow t 2.0)))) r))))
\begin{array}{l}

\\
\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right)
\end{array}

Alternative 1: 99.2% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \frac{\mathsf{fma}\left(\frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \cdot \frac{0.25 \cdot a}{r}}{\mathsf{PI}\left(\right) \cdot r} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (/
  (*
   (fma (/ r (exp (pow (/ t r) -2.0))) (/ -2.0 (sqrt (PI))) (erf (/ r t)))
   (/ (* 0.25 a) r))
  (* (PI) r)))
\begin{array}{l}

\\
\frac{\mathsf{fma}\left(\frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \cdot \frac{0.25 \cdot a}{r}}{\mathsf{PI}\left(\right) \cdot r}
\end{array}
Derivation

  1. Initial program 99.1%

    \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation

    1. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    2. lift-/.f64N/A

      \[\leadsto \left(\color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    3. lift-/.f64N/A

      \[\leadsto \left(\frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    4. associate-/l/N/A

      \[\leadsto \left(\color{blue}{\frac{\frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    5. associate-*l/N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    6. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    7. *-commutativeN/A

      \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    8. lower-*.f64N/A

      \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    9. lift-/.f64N/A

      \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    10. metadata-evalN/A

      \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    11. lower-*.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\color{blue}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    12. lift-pow.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{{r}^{2}} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    13. unpow2N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    14. lower-*.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

  4. Applied rewrites99.2%

    \[\leadsto \color{blue}{\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

  6. Applied rewrites99.3%

    \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \cdot \frac{0.25 \cdot a}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]
  7. Add Preprocessing

Alternative 2: 88.9% accurate, 2.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\ \mathbf{if}\;r \leq 0.0028:\\ \;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(\sqrt{{\mathsf{PI}\left(\right)}^{-1}} \cdot \mathsf{fma}\left(\frac{2}{t}, \frac{r \cdot r}{t}, -2\right), r, t\_1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{\mathsf{PI}\left(\right) \cdot r}\\ \end{array} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (let* ((t_1 (erf (/ r t))))
   (if (<= r 0.0028)
     (*
      (/ (* a 0.25) (* (* r r) (PI)))
      (fma
       (* (sqrt (pow (PI) -1.0)) (fma (/ 2.0 t) (/ (* r r) t) -2.0))
       r
       t_1))
     (/ (/ (* (* 0.25 a) t_1) r) (* (PI) r)))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\
\mathbf{if}\;r \leq 0.0028:\\
\;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(\sqrt{{\mathsf{PI}\left(\right)}^{-1}} \cdot \mathsf{fma}\left(\frac{2}{t}, \frac{r \cdot r}{t}, -2\right), r, t\_1\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{\mathsf{PI}\left(\right) \cdot r}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if r < 0.00279999999999999997

    1. Initial program 99.0%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation

      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      2. lift-/.f64N/A

        \[\leadsto \left(\color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      3. lift-/.f64N/A

        \[\leadsto \left(\frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      4. associate-/l/N/A

        \[\leadsto \left(\color{blue}{\frac{\frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      5. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      7. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      8. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      9. lift-/.f64N/A

        \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      10. metadata-evalN/A

        \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      11. lower-*.f6499.0

        \[\leadsto \frac{a \cdot 0.25}{\color{blue}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      12. lift-pow.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{{r}^{2}} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      13. unpow2N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      14. lower-*.f6499.0

        \[\leadsto \frac{a \cdot 0.25}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    4. Applied rewrites99.0%

      \[\leadsto \color{blue}{\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + r \cdot \left(2 \cdot \left(\frac{{r}^{2}}{{t}^{2}} \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) - 2 \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)} \]
    6. Step-by-step derivation

      1. +-commutativeN/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\left(r \cdot \left(2 \cdot \left(\frac{{r}^{2}}{{t}^{2}} \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) - 2 \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) + \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

      2. *-commutativeN/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\color{blue}{\left(2 \cdot \left(\frac{{r}^{2}}{{t}^{2}} \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) - 2 \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) \cdot r} + \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      3. lower-fma.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\mathsf{fma}\left(2 \cdot \left(\frac{{r}^{2}}{{t}^{2}} \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) - 2 \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, r, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

    7. Applied rewrites76.7%

      \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\mathsf{fma}\left(\sqrt{\frac{1}{\mathsf{PI}\left(\right)}} \cdot \mathsf{fma}\left(\frac{2}{t}, \frac{r \cdot r}{t}, -2\right), r, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

    if 0.00279999999999999997 < r

    1. Initial program 99.2%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites99.4%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{\frac{\color{blue}{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
    6. Step-by-step derivation

      1. associate-*r*N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      2. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      3. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right)} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      4. lower-erf.f64N/A

        \[\leadsto \frac{\frac{\left(\frac{1}{4} \cdot a\right) \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      5. lower-/.f6493.4

        \[\leadsto \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    7. Applied rewrites93.4%

      \[\leadsto \frac{\frac{\color{blue}{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification87.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;r \leq 0.0028:\\ \;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(\sqrt{{\mathsf{PI}\left(\right)}^{-1}} \cdot \mathsf{fma}\left(\frac{2}{t}, \frac{r \cdot r}{t}, -2\right), r, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 99.2% accurate, 2.0× speedup?

\[\begin{array}{l} \\ \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\left(-r\right) \cdot r}{t \cdot t}}\right) \cdot r\right) \end{array} \]
(FPCore (r a t)
 :precision binary64
 (*
  (/ (* a 0.25) (* (* r r) (PI)))
  (-
   (erf (/ r t))
   (* (* (/ 2.0 (sqrt (PI))) (exp (/ (* (- r) r) (* t t)))) r))))
\begin{array}{l}

\\
\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\left(-r\right) \cdot r}{t \cdot t}}\right) \cdot r\right)
\end{array}
Derivation

  1. Initial program 99.1%

    \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation

    1. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    2. lift-/.f64N/A

      \[\leadsto \left(\color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    3. lift-/.f64N/A

      \[\leadsto \left(\frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    4. associate-/l/N/A

      \[\leadsto \left(\color{blue}{\frac{\frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    5. associate-*l/N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    6. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    7. *-commutativeN/A

      \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    8. lower-*.f64N/A

      \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    9. lift-/.f64N/A

      \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    10. metadata-evalN/A

      \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    11. lower-*.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\color{blue}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    12. lift-pow.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{{r}^{2}} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    13. unpow2N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    14. lower-*.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

  4. Applied rewrites99.2%

    \[\leadsto \color{blue}{\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
  5. Step-by-step derivation

    1. lift-neg.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\color{blue}{\mathsf{neg}\left({r}^{2}\right)}}{{t}^{2}}}\right) \cdot r\right) \]

    2. lift-pow.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\mathsf{neg}\left(\color{blue}{{r}^{2}}\right)}{{t}^{2}}}\right) \cdot r\right) \]

    3. pow2N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\mathsf{neg}\left(\color{blue}{r \cdot r}\right)}{{t}^{2}}}\right) \cdot r\right) \]

    4. distribute-lft-neg-inN/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\color{blue}{\left(\mathsf{neg}\left(r\right)\right) \cdot r}}{{t}^{2}}}\right) \cdot r\right) \]

    5. lower-*.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\color{blue}{\left(\mathsf{neg}\left(r\right)\right) \cdot r}}{{t}^{2}}}\right) \cdot r\right) \]

    6. lower-neg.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\color{blue}{\left(-r\right)} \cdot r}{{t}^{2}}}\right) \cdot r\right) \]

    7. lift-pow.f64N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\left(-r\right) \cdot r}{\color{blue}{{t}^{2}}}}\right) \cdot r\right) \]

    8. unpow2N/A

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\left(-r\right) \cdot r}{\color{blue}{t \cdot t}}}\right) \cdot r\right) \]

    9. lower-*.f6499.2

      \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{\left(-r\right) \cdot r}{\color{blue}{t \cdot t}}}\right) \cdot r\right) \]

  6. Applied rewrites99.2%

    \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\color{blue}{\frac{\left(-r\right) \cdot r}{t \cdot t}}}\right) \cdot r\right) \]
  7. Add Preprocessing

Alternative 4: 85.2% accurate, 2.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\ t_2 := \mathsf{PI}\left(\right) \cdot r\\ \mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{\mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, t\_1\right)}{t\_2} \cdot \frac{0.25 \cdot a}{r}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{t\_2}\\ \end{array} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (let* ((t_1 (erf (/ r t))) (t_2 (* (PI) r)))
   (if (<= r 3.8e-5)
     (* (/ (fma (* -2.0 r) (sqrt (pow (PI) -1.0)) t_1) t_2) (/ (* 0.25 a) r))
     (/ (/ (* (* 0.25 a) t_1) r) t_2))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\
t_2 := \mathsf{PI}\left(\right) \cdot r\\
\mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\
\;\;\;\;\frac{\mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, t\_1\right)}{t\_2} \cdot \frac{0.25 \cdot a}{r}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{t\_2}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if r < 3.8000000000000002e-5

    1. Initial program 99.0%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites98.8%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in t around inf

      \[\leadsto \color{blue}{\frac{1}{4} \cdot \frac{a \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + -2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]
    6. Step-by-step derivation

      1. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot \left(a \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + -2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]

      2. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{\left(a \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + -2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)\right) \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      3. metadata-evalN/A

        \[\leadsto \frac{\left(a \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(2\right)\right)} \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)\right) \cdot \frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      4. cancel-sign-sub-invN/A

        \[\leadsto \frac{\left(a \cdot \color{blue}{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)}\right) \cdot \frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      5. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{\left(\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot a\right)} \cdot \frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      6. associate-*l*N/A

        \[\leadsto \frac{\color{blue}{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(a \cdot \frac{1}{4}\right)}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      7. *-commutativeN/A

        \[\leadsto \frac{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \color{blue}{\left(\frac{1}{4} \cdot a\right)}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \]

      8. *-commutativeN/A

        \[\leadsto \frac{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(\frac{1}{4} \cdot a\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot {r}^{2}}} \]

      9. unpow2N/A

        \[\leadsto \frac{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(\frac{1}{4} \cdot a\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{\left(r \cdot r\right)}} \]

      10. associate-*r*N/A

        \[\leadsto \frac{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(\frac{1}{4} \cdot a\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot r\right) \cdot r}} \]

      11. *-commutativeN/A

        \[\leadsto \frac{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - 2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(\frac{1}{4} \cdot a\right)}{\color{blue}{\left(r \cdot \mathsf{PI}\left(\right)\right)} \cdot r} \]

    7. Applied rewrites76.0%

      \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\mathsf{PI}\left(\right) \cdot r} \cdot \frac{0.25 \cdot a}{r}} \]

    if 3.8000000000000002e-5 < r

    1. Initial program 99.2%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites99.3%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{\frac{\color{blue}{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
    6. Step-by-step derivation

      1. associate-*r*N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      2. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      3. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right)} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      4. lower-erf.f64N/A

        \[\leadsto \frac{\frac{\left(\frac{1}{4} \cdot a\right) \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      5. lower-/.f6486.5

        \[\leadsto \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    7. Applied rewrites86.5%

      \[\leadsto \frac{\frac{\color{blue}{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification84.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{\mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\mathsf{PI}\left(\right) \cdot r} \cdot \frac{0.25 \cdot a}{r}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}\\ \end{array} \]
  5. Add Preprocessing

Alternative 5: 85.2% accurate, 2.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\ \mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, t\_1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{\mathsf{PI}\left(\right) \cdot r}\\ \end{array} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (let* ((t_1 (erf (/ r t))))
   (if (<= r 3.8e-5)
     (*
      (/ (* a 0.25) (* (* r r) (PI)))
      (fma (* -2.0 r) (sqrt (pow (PI) -1.0)) t_1))
     (/ (/ (* (* 0.25 a) t_1) r) (* (PI) r)))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\
\mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\
\;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, t\_1\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{\mathsf{PI}\left(\right) \cdot r}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if r < 3.8000000000000002e-5

    1. Initial program 99.0%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation

      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      2. lift-/.f64N/A

        \[\leadsto \left(\color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      3. lift-/.f64N/A

        \[\leadsto \left(\frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      4. associate-/l/N/A

        \[\leadsto \left(\color{blue}{\frac{\frac{1}{4}}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      5. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot a}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      7. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      8. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{a \cdot \frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      9. lift-/.f64N/A

        \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      10. metadata-evalN/A

        \[\leadsto \frac{a \cdot \color{blue}{\frac{1}{4}}}{{r}^{2} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      11. lower-*.f6498.9

        \[\leadsto \frac{a \cdot 0.25}{\color{blue}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      12. lift-pow.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{{r}^{2}} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      13. unpow2N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

      14. lower-*.f6498.9

        \[\leadsto \frac{a \cdot 0.25}{\color{blue}{\left(r \cdot r\right)} \cdot \mathsf{PI}\left(\right)} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    4. Applied rewrites98.9%

      \[\leadsto \color{blue}{\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}} \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) + -2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right)\right)} \]
    6. Step-by-step derivation

      1. +-commutativeN/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\left(-2 \cdot \left(r \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}\right) + \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

      2. associate-*r*N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \left(\color{blue}{\left(-2 \cdot r\right) \cdot \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}} + \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      3. lower-fma.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

      4. lower-*.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(\color{blue}{-2 \cdot r}, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      5. lower-sqrt.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \color{blue}{\sqrt{\frac{1}{\mathsf{PI}\left(\right)}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      6. lower-/.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{\color{blue}{\frac{1}{\mathsf{PI}\left(\right)}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      7. lower-PI.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\color{blue}{\mathsf{PI}\left(\right)}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      8. lower-erf.f64N/A

        \[\leadsto \frac{a \cdot \frac{1}{4}}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}\right) \]

      9. lower-/.f6476.0

        \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)\right) \]

    7. Applied rewrites76.0%

      \[\leadsto \frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \color{blue}{\mathsf{fma}\left(-2 \cdot r, \sqrt{\frac{1}{\mathsf{PI}\left(\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

    if 3.8000000000000002e-5 < r

    1. Initial program 99.2%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites99.3%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{\frac{\color{blue}{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
    6. Step-by-step derivation

      1. associate-*r*N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      2. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      3. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right)} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      4. lower-erf.f64N/A

        \[\leadsto \frac{\frac{\left(\frac{1}{4} \cdot a\right) \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      5. lower-/.f6486.5

        \[\leadsto \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    7. Applied rewrites86.5%

      \[\leadsto \frac{\frac{\color{blue}{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification84.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;r \leq 3.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{a \cdot 0.25}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \cdot \mathsf{fma}\left(-2 \cdot r, \sqrt{{\mathsf{PI}\left(\right)}^{-1}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}\\ \end{array} \]
  5. Add Preprocessing

Alternative 6: 90.0% accurate, 2.7× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\ t_2 := \mathsf{PI}\left(\right) \cdot r\\ \mathbf{if}\;r \leq 0.003:\\ \;\;\;\;\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\mathsf{fma}\left(\frac{r}{t}, \frac{r}{t}, 1\right)}, t\_1\right)}{r}}{t\_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{t\_2}\\ \end{array} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (let* ((t_1 (erf (/ r t))) (t_2 (* (PI) r)))
   (if (<= r 0.003)
     (/
      (/
       (*
        (* a 0.25)
        (fma (/ -2.0 (sqrt (PI))) (/ r (fma (/ r t) (/ r t) 1.0)) t_1))
       r)
      t_2)
     (/ (/ (* (* 0.25 a) t_1) r) t_2))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\\
t_2 := \mathsf{PI}\left(\right) \cdot r\\
\mathbf{if}\;r \leq 0.003:\\
\;\;\;\;\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\mathsf{fma}\left(\frac{r}{t}, \frac{r}{t}, 1\right)}, t\_1\right)}{r}}{t\_2}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\left(0.25 \cdot a\right) \cdot t\_1}{r}}{t\_2}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if r < 0.0030000000000000001

    1. Initial program 99.0%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites98.9%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\color{blue}{1 + \frac{{r}^{2}}{{t}^{2}}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
    6. Step-by-step derivation

      1. +-commutativeN/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\color{blue}{\frac{{r}^{2}}{{t}^{2}} + 1}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      2. unpow2N/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\frac{\color{blue}{r \cdot r}}{{t}^{2}} + 1}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      3. unpow2N/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\frac{r \cdot r}{\color{blue}{t \cdot t}} + 1}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      4. times-fracN/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\color{blue}{\frac{r}{t} \cdot \frac{r}{t}} + 1}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      5. lower-fma.f64N/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\color{blue}{\mathsf{fma}\left(\frac{r}{t}, \frac{r}{t}, 1\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      6. lower-/.f64N/A

        \[\leadsto \frac{\frac{\left(a \cdot \frac{1}{4}\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\mathsf{fma}\left(\color{blue}{\frac{r}{t}}, \frac{r}{t}, 1\right)}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      7. lower-/.f6479.4

        \[\leadsto \frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\mathsf{fma}\left(\frac{r}{t}, \color{blue}{\frac{r}{t}}, 1\right)}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    7. Applied rewrites79.4%

      \[\leadsto \frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{\color{blue}{\mathsf{fma}\left(\frac{r}{t}, \frac{r}{t}, 1\right)}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    if 0.0030000000000000001 < r

    1. Initial program 99.2%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    4. Applied rewrites99.4%

      \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

    5. Taylor expanded in r around 0

      \[\leadsto \frac{\frac{\color{blue}{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
    6. Step-by-step derivation

      1. associate-*r*N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      2. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      3. lower-*.f64N/A

        \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right)} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      4. lower-erf.f64N/A

        \[\leadsto \frac{\frac{\left(\frac{1}{4} \cdot a\right) \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

      5. lower-/.f6493.4

        \[\leadsto \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    7. Applied rewrites93.4%

      \[\leadsto \frac{\frac{\color{blue}{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 7: 73.2% accurate, 4.1× speedup?

\[\begin{array}{l} \\ \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (/ (/ (* (* 0.25 a) (erf (/ r t))) r) (* (PI) r)))
\begin{array}{l}

\\
\frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}
\end{array}
Derivation

  1. Initial program 99.1%

    \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
  2. Add Preprocessing

  4. Applied rewrites99.2%

    \[\leadsto \color{blue}{\frac{\frac{\left(a \cdot 0.25\right) \cdot \mathsf{fma}\left(\frac{-2}{\sqrt{\mathsf{PI}\left(\right)}}, \frac{r}{e^{{\left(\frac{t}{r}\right)}^{-2}}}, \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r}} \]

  5. Taylor expanded in r around 0

    \[\leadsto \frac{\frac{\color{blue}{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  6. Step-by-step derivation

    1. associate-*r*N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    2. lower-*.f64N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    3. lower-*.f64N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(\frac{1}{4} \cdot a\right)} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    4. lower-erf.f64N/A

      \[\leadsto \frac{\frac{\left(\frac{1}{4} \cdot a\right) \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

    5. lower-/.f6474.2

      \[\leadsto \frac{\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)}{r}}{\mathsf{PI}\left(\right) \cdot r} \]

  7. Applied rewrites74.2%

    \[\leadsto \frac{\frac{\color{blue}{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}}{r}}{\mathsf{PI}\left(\right) \cdot r} \]
  8. Add Preprocessing

Alternative 8: 73.2% accurate, 4.2× speedup?

\[\begin{array}{l} \\ \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\left(r \cdot \left(\mathsf{PI}\left(\right) \cdot 4\right)\right) \cdot r} \end{array} \]
(FPCore (r a t)
 :precision binary64
 (/ (* a (erf (/ r t))) (* (* r (* (PI) 4.0)) r)))
\begin{array}{l}

\\
\frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\left(r \cdot \left(\mathsf{PI}\left(\right) \cdot 4\right)\right) \cdot r}
\end{array}
Derivation

  1. Initial program 99.1%

    \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
  2. Add Preprocessing

  3. Taylor expanded in r around 0

    \[\leadsto \color{blue}{\frac{1}{4} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]
  4. Step-by-step derivation

    1. associate-*r/N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]

    2. *-commutativeN/A

      \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot {r}^{2}}} \]

    3. unpow2N/A

      \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{\left(r \cdot r\right)}} \]

    4. associate-*r*N/A

      \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot r\right) \cdot r}} \]

    5. *-commutativeN/A

      \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\left(r \cdot \mathsf{PI}\left(\right)\right)} \cdot r} \]

    6. times-fracN/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4}}{r \cdot \mathsf{PI}\left(\right)} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}} \]

    7. lower-*.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{4}}{r \cdot \mathsf{PI}\left(\right)} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}} \]

    8. *-commutativeN/A

      \[\leadsto \frac{\frac{1}{4}}{\color{blue}{\mathsf{PI}\left(\right) \cdot r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

    9. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

    10. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

    11. lower-/.f64N/A

      \[\leadsto \frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{r} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

    12. lower-PI.f64N/A

      \[\leadsto \frac{\frac{\frac{1}{4}}{\color{blue}{\mathsf{PI}\left(\right)}}}{r} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

    13. associate-*l/N/A

      \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \color{blue}{\left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

    14. lower-*.f64N/A

      \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \color{blue}{\left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

    15. lower-/.f64N/A

      \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\color{blue}{\frac{a}{r}} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

    16. lower-erf.f64N/A

      \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}\right) \]

    17. lower-/.f6474.1

      \[\leadsto \frac{\frac{0.25}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)\right) \]

  5. Applied rewrites74.1%

    \[\leadsto \color{blue}{\frac{\frac{0.25}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]
  6. Step-by-step derivation

    1. Applied rewrites74.2%

      \[\leadsto \frac{1 \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\left(r \cdot \left(\mathsf{PI}\left(\right) \cdot 4\right)\right) \cdot r}} \]

    2. Final simplification74.2%

      \[\leadsto \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\left(r \cdot \left(\mathsf{PI}\left(\right) \cdot 4\right)\right) \cdot r} \]
    3. Add Preprocessing

    Alternative 9: 73.2% accurate, 4.2× speedup?

    \[\begin{array}{l} \\ \frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)} \end{array} \]
    (FPCore (r a t)
 :precision binary64
 (/ (* (* 0.25 a) (erf (/ r t))) (* (* r r) (PI))))
    \begin{array}{l}

\\
\frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}
\end{array}
    Derivation

    1. Initial program 99.1%

      \[\left(\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{{r}^{2}} \cdot a\right) \cdot \left(\mathsf{erf}\left(\left(\frac{r}{t}\right)\right) - \left(\frac{2}{\sqrt{\mathsf{PI}\left(\right)}} \cdot e^{\frac{-{r}^{2}}{{t}^{2}}}\right) \cdot r\right) \]
    2. Add Preprocessing

    3. Taylor expanded in r around 0

      \[\leadsto \color{blue}{\frac{1}{4} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]
    4. Step-by-step derivation

      1. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{{r}^{2} \cdot \mathsf{PI}\left(\right)}} \]

      2. *-commutativeN/A

        \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot {r}^{2}}} \]

      3. unpow2N/A

        \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{\left(r \cdot r\right)}} \]

      4. associate-*r*N/A

        \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\left(\mathsf{PI}\left(\right) \cdot r\right) \cdot r}} \]

      5. *-commutativeN/A

        \[\leadsto \frac{\frac{1}{4} \cdot \left(a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)}{\color{blue}{\left(r \cdot \mathsf{PI}\left(\right)\right)} \cdot r} \]

      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4}}{r \cdot \mathsf{PI}\left(\right)} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}} \]

      7. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{4}}{r \cdot \mathsf{PI}\left(\right)} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r}} \]

      8. *-commutativeN/A

        \[\leadsto \frac{\frac{1}{4}}{\color{blue}{\mathsf{PI}\left(\right) \cdot r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

      9. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

      10. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r}} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

      11. lower-/.f64N/A

        \[\leadsto \frac{\color{blue}{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}}{r} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

      12. lower-PI.f64N/A

        \[\leadsto \frac{\frac{\frac{1}{4}}{\color{blue}{\mathsf{PI}\left(\right)}}}{r} \cdot \frac{a \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{r} \]

      13. associate-*l/N/A

        \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \color{blue}{\left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

      14. lower-*.f64N/A

        \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \color{blue}{\left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]

      15. lower-/.f64N/A

        \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\color{blue}{\frac{a}{r}} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right) \]

      16. lower-erf.f64N/A

        \[\leadsto \frac{\frac{\frac{1}{4}}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \color{blue}{\mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}\right) \]

      17. lower-/.f6474.1

        \[\leadsto \frac{\frac{0.25}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \mathsf{erf}\left(\color{blue}{\left(\frac{r}{t}\right)}\right)\right) \]

    5. Applied rewrites74.1%

      \[\leadsto \color{blue}{\frac{\frac{0.25}{\mathsf{PI}\left(\right)}}{r} \cdot \left(\frac{a}{r} \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)\right)} \]
    6. Step-by-step derivation

      1. Applied rewrites74.2%

        \[\leadsto \frac{\left(0.25 \cdot a\right) \cdot \mathsf{erf}\left(\left(\frac{r}{t}\right)\right)}{\color{blue}{\left(r \cdot r\right) \cdot \mathsf{PI}\left(\right)}} \]
      2. Add Preprocessing

      Reproduce

      ?
      herbie shell --seed 1 
(FPCore (r a t)
  :name "1 / 4 / PI / r^2 * a * (erf(r / t) - 2 / sqrt(PI) * exp(- r^2 / t^2) * r)"
  :precision binary64
  :pre (and (and (and (<= 1e-10 r) (<= r 10000000000.0)) (and (<= 0.0 a) (<= a 1.0))) (and (<= 1e-6 t) (<= t 1.0)))
  (* (* (/ (/ (/ 1.0 4.0) (PI)) (pow r 2.0)) a) (- (erf (/ r t)) (* (* (/ 2.0 (sqrt (PI))) (exp (/ (- (pow r 2.0)) (pow t 2.0)))) r))))