Average Error: 60.8 → 29.6
Time: 18.8s
Precision: 64
\[1 \le y \le 9999\]
\[\begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
\[\begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right) + \left(\frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)} + \frac{-\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right)}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
\begin{array}{l}
\mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\frac{e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\

\end{array}
\begin{array}{l}
\mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right) + \left(\frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)} + \frac{-\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right)}\right) = 0.0:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\

\end{array}
double f(double y) {
        double r103778 = y;
        double r103779 = r103778 * r103778;
        double r103780 = 1.0;
        double r103781 = r103779 + r103780;
        double r103782 = sqrt(r103781);
        double r103783 = r103778 - r103782;
        double r103784 = fabs(r103783);
        double r103785 = r103778 + r103782;
        double r103786 = r103780 / r103785;
        double r103787 = r103784 - r103786;
        double r103788 = r103787 * r103787;
        double r103789 = 0.0;
        double r103790 = r103788 == r103789;
        double r103791 = exp(r103788);
        double r103792 = r103791 - r103780;
        double r103793 = r103792 / r103788;
        double r103794 = r103790 ? r103780 : r103793;
        return r103794;
}

double f(double y) {
        double r103795 = y;
        double r103796 = r103795 * r103795;
        double r103797 = 1.0;
        double r103798 = r103796 + r103797;
        double r103799 = sqrt(r103798);
        double r103800 = r103795 - r103799;
        double r103801 = fabs(r103800);
        double r103802 = r103795 + r103799;
        double r103803 = r103797 / r103802;
        double r103804 = r103801 - r103803;
        double r103805 = r103800 * r103797;
        double r103806 = fma(r103795, r103795, r103797);
        double r103807 = -r103806;
        double r103808 = fma(r103795, r103795, r103807);
        double r103809 = r103805 / r103808;
        double r103810 = r103801 - r103809;
        double r103811 = -r103805;
        double r103812 = r103811 / r103808;
        double r103813 = r103809 + r103812;
        double r103814 = r103810 + r103813;
        double r103815 = exp(r103814);
        double r103816 = log(r103815);
        double r103817 = r103804 * r103816;
        double r103818 = 0.0;
        double r103819 = r103817 == r103818;
        double r103820 = 0.5;
        double r103821 = 1.0;
        double r103822 = r103821 / r103795;
        double r103823 = 2.0;
        double r103824 = 2.0;
        double r103825 = pow(r103795, r103824);
        double r103826 = r103825 + r103797;
        double r103827 = sqrt(r103826);
        double r103828 = r103795 - r103827;
        double r103829 = fabs(r103828);
        double r103830 = fma(r103823, r103795, r103829);
        double r103831 = fma(r103820, r103822, r103830);
        double r103832 = r103831 * r103804;
        double r103833 = exp(r103832);
        double r103834 = r103833 - r103797;
        double r103835 = r103834 / r103832;
        double r103836 = r103819 ? r103797 : r103835;
        return r103836;
}

Error

Bits error versus y

Derivation

  1. Initial program 60.8

    \[\begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  2. Taylor expanded around -inf 59.2

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\left(0.5 \cdot \frac{1}{y} + \left(2 \cdot y + \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  3. Simplified59.2

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  4. Taylor expanded around -inf 37.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\color{blue}{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}}{\left(0.5 \cdot \frac{1}{y} + \left(2 \cdot y + \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  5. Simplified37.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\color{blue}{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  6. Using strategy rm
  7. Applied add-log-exp36.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \color{blue}{\log \left(e^{\frac{1}{y + \sqrt{y \cdot y + 1}}}\right)}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  8. Applied add-log-exp33.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \left(\color{blue}{\log \left(e^{\left|y - \sqrt{y \cdot y + 1}\right|}\right)} - \log \left(e^{\frac{1}{y + \sqrt{y \cdot y + 1}}}\right)\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  9. Applied diff-log33.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \color{blue}{\log \left(\frac{e^{\left|y - \sqrt{y \cdot y + 1}\right|}}{e^{\frac{1}{y + \sqrt{y \cdot y + 1}}}}\right)} = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  10. Simplified33.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \color{blue}{\left(e^{\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}}\right)} = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  11. Using strategy rm
  12. Applied flip-+18.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{\color{blue}{\frac{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}{y - \sqrt{y \cdot y + 1}}}}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  13. Applied associate-/r/18.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left|y - \sqrt{y \cdot y + 1}\right| - \color{blue}{\frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}} \cdot \left(y - \sqrt{y \cdot y + 1}\right)}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  14. Applied add-sqr-sqrt17.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\color{blue}{\sqrt{\left|y - \sqrt{y \cdot y + 1}\right|} \cdot \sqrt{\left|y - \sqrt{y \cdot y + 1}\right|}} - \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}} \cdot \left(y - \sqrt{y \cdot y + 1}\right)}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  15. Applied prod-diff18.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\color{blue}{\mathsf{fma}\left(\sqrt{\left|y - \sqrt{y \cdot y + 1}\right|}, \sqrt{\left|y - \sqrt{y \cdot y + 1}\right|}, -\left(y - \sqrt{y \cdot y + 1}\right) \cdot \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}\right) + \mathsf{fma}\left(-\left(y - \sqrt{y \cdot y + 1}\right), \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}, \left(y - \sqrt{y \cdot y + 1}\right) \cdot \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}\right)}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  16. Simplified29.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\color{blue}{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right)} + \mathsf{fma}\left(-\left(y - \sqrt{y \cdot y + 1}\right), \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}, \left(y - \sqrt{y \cdot y + 1}\right) \cdot \frac{1}{y \cdot y - \sqrt{y \cdot y + 1} \cdot \sqrt{y \cdot y + 1}}\right)}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  17. Simplified29.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right) + \color{blue}{\left(\frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)} + \frac{-\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right)}}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]
  18. Final simplification29.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right) \cdot \log \left(e^{\left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right) + \left(\frac{\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)} + \frac{-\left(y - \sqrt{y \cdot y + 1}\right) \cdot 1}{\mathsf{fma}\left(y, y, -\mathsf{fma}\left(y, y, 1\right)\right)}\right)}\right) = 0.0:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)} - 1}{\mathsf{fma}\left(0.5, \frac{1}{y}, \mathsf{fma}\left(2, y, \left|y - \sqrt{{y}^{2} + 1}\right|\right)\right) \cdot \left(\left|y - \sqrt{y \cdot y + 1}\right| - \frac{1}{y + \sqrt{y \cdot y + 1}}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2020033 +o rules:numerics
(FPCore (y)
  :name "Kahan's Monster"
  :precision binary64
  :pre (<= 1 y 9999)
  (if (== (* (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1))))) (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1)))))) 0.0) 1 (/ (- (exp (* (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1))))) (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1))))))) 1) (* (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1))))) (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1)))))))))