Average Error: 0.0 → 5.4
Time: 9.9s
Precision: 64
\[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y \cdot \left(-x \cdot y\right)}{\left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right) \cdot 2}\\ \end{array}\]
x - \frac{y}{1 + \frac{x \cdot y}{2}}
↓
\begin{array}{l}
\mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\
\;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\

\mathbf{else}:\\
\;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y \cdot \left(-x \cdot y\right)}{\left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right) \cdot 2}\\

\end{array}
double f(double x, double y) {
        double r348582 = x;
        double r348583 = y;
        double r348584 = 1.0;
        double r348585 = r348582 * r348583;
        double r348586 = 2.0;
        double r348587 = r348585 / r348586;
        double r348588 = r348584 + r348587;
        double r348589 = r348583 / r348588;
        double r348590 = r348582 - r348589;
        return r348590;
}
↓
double f(double x, double y) {
        double r348591 = y;
        double r348592 = -1.0316187449465748e+92;
        bool r348593 = r348591 <= r348592;
        double r348594 = 1.2105836526692892e+131;
        bool r348595 = r348591 <= r348594;
        double r348596 = !r348595;
        bool r348597 = r348593 || r348596;
        double r348598 = x;
        double r348599 = 1.0;
        double r348600 = r348599 * r348599;
        double r348601 = r348598 * r348591;
        double r348602 = 2.0;
        double r348603 = r348601 / r348602;
        double r348604 = r348603 * r348603;
        double r348605 = r348600 - r348604;
        double r348606 = r348591 / r348605;
        double r348607 = r348606 * r348599;
        double r348608 = r348598 - r348607;
        double r348609 = r348602 / r348598;
        double r348610 = r348608 - r348609;
        double r348611 = -r348601;
        double r348612 = r348591 * r348611;
        double r348613 = r348605 * r348602;
        double r348614 = r348612 / r348613;
        double r348615 = r348608 - r348614;
        double r348616 = r348597 ? r348610 : r348615;
        return r348616;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 2 regimes

  2. if y < -1.0316187449465748e+92 or 1.2105836526692892e+131 < y

    1. Initial program 0.1

      \[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
    2. Using strategy rm

    3. Applied flip-+27.4

      \[\leadsto x - \frac{y}{\color{blue}{\frac{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}}{1 - \frac{x \cdot y}{2}}}}\]

    4. Applied associate-/r/27.5

      \[\leadsto x - \color{blue}{\frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(1 - \frac{x \cdot y}{2}\right)}\]
    5. Using strategy rm

    6. Applied sub-neg27.5

      \[\leadsto x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \color{blue}{\left(1 + \left(-\frac{x \cdot y}{2}\right)\right)}\]

    7. Applied distribute-lft-in27.4

      \[\leadsto x - \color{blue}{\left(\frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1 + \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(-\frac{x \cdot y}{2}\right)\right)}\]

    8. Applied associate--r+27.4

      \[\leadsto \color{blue}{\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(-\frac{x \cdot y}{2}\right)}\]

    9. Taylor expanded around inf 10.4

      \[\leadsto \left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \color{blue}{\frac{2}{x}}\]

    if -1.0316187449465748e+92 < y < 1.2105836526692892e+131

    1. Initial program 0.0

      \[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
    2. Using strategy rm

    3. Applied flip-+1.8

      \[\leadsto x - \frac{y}{\color{blue}{\frac{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}}{1 - \frac{x \cdot y}{2}}}}\]

    4. Applied associate-/r/1.8

      \[\leadsto x - \color{blue}{\frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(1 - \frac{x \cdot y}{2}\right)}\]
    5. Using strategy rm

    6. Applied sub-neg1.8

      \[\leadsto x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \color{blue}{\left(1 + \left(-\frac{x \cdot y}{2}\right)\right)}\]

    7. Applied distribute-lft-in1.8

      \[\leadsto x - \color{blue}{\left(\frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1 + \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(-\frac{x \cdot y}{2}\right)\right)}\]

    8. Applied associate--r+1.8

      \[\leadsto \color{blue}{\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \left(-\frac{x \cdot y}{2}\right)}\]
    9. Using strategy rm

    10. Applied distribute-neg-frac1.8

      \[\leadsto \left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot \color{blue}{\frac{-x \cdot y}{2}}\]

    11. Applied frac-times3.2

      \[\leadsto \left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \color{blue}{\frac{y \cdot \left(-x \cdot y\right)}{\left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right) \cdot 2}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification5.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{y \cdot \left(-x \cdot y\right)}{\left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right) \cdot 2}\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 
(FPCore (x y)
  :name "Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, B"
  :precision binary64
  (- x (/ y (+ 1 (/ (* x y) 2)))))