\[0.0 \lt x \lt 1 \land y \lt 1\]

\[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;y \le -5.797856225877881060769082412965027708037 \cdot 10^{150}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -1.329253761175223739159446383274506990081 \cdot 10^{-158}:\\ \;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\ \mathbf{elif}\;y \le 7.961862811311691246218405838467989119993 \cdot 10^{-164}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\ \end{array}\]

\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}

↓

\begin{array}{l}
\mathbf{if}\;y \le -5.797856225877881060769082412965027708037 \cdot 10^{150}:\\
\;\;\;\;-1\\

\mathbf{elif}\;y \le -1.329253761175223739159446383274506990081 \cdot 10^{-158}:\\
\;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\

\mathbf{elif}\;y \le 7.961862811311691246218405838467989119993 \cdot 10^{-164}:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\

\end{array}

double f(double x, double y) {
        double r5405607 = x;
        double r5405608 = y;
        double r5405609 = r5405607 - r5405608;
        double r5405610 = r5405607 + r5405608;
        double r5405611 = r5405609 * r5405610;
        double r5405612 = r5405607 * r5405607;
        double r5405613 = r5405608 * r5405608;
        double r5405614 = r5405612 + r5405613;
        double r5405615 = r5405611 / r5405614;
        return r5405615;
}

↓

double f(double x, double y) {
        double r5405616 = y;
        double r5405617 = -5.797856225877881e+150;
        bool r5405618 = r5405616 <= r5405617;
        double r5405619 = -1.0;
        double r5405620 = -1.3292537611752237e-158;
        bool r5405621 = r5405616 <= r5405620;
        double r5405622 = x;
        double r5405623 = r5405622 * r5405622;
        double r5405624 = r5405616 * r5405616;
        double r5405625 = r5405623 + r5405624;
        double r5405626 = sqrt(r5405625);
        double r5405627 = r5405623 / r5405626;
        double r5405628 = r5405616 / r5405626;
        double r5405629 = r5405616 * r5405628;
        double r5405630 = r5405627 - r5405629;
        double r5405631 = r5405630 / r5405626;
        double r5405632 = 7.961862811311691e-164;
        bool r5405633 = r5405616 <= r5405632;
        double r5405634 = 1.0;
        double r5405635 = r5405633 ? r5405634 : r5405631;
        double r5405636 = r5405621 ? r5405631 : r5405635;
        double r5405637 = r5405618 ? r5405619 : r5405636;
        return r5405637;
}

Original	20.1
Target	0.0
Herbie	5.0

Derivation

Split input into 3 regimes
if y < -5.797856225877881e+150
1. Initial program 62.3
  \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
2. Taylor expanded around 0 0
  \[\leadsto \color{blue}{-1}\]
if -5.797856225877881e+150 < y < -1.3292537611752237e-158 or 7.961862811311691e-164 < y
1. Initial program 0.1
  \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
2. Using strategy rm
3. Applied add-sqr-sqrt0.1
  \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\color{blue}{\sqrt{x \cdot x + y \cdot y} \cdot \sqrt{x \cdot x + y \cdot y}}}\]
4. Applied associate-/r*0.2
  \[\leadsto \color{blue}{\frac{\frac{\left(x - y\right) \cdot \left(x + y\right)}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}}\]
5. Simplified0.2
  \[\leadsto \frac{\color{blue}{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - \frac{y \cdot y}{\sqrt{x \cdot x + y \cdot y}}}}{\sqrt{x \cdot x + y \cdot y}}\]
6. Using strategy rm
7. Applied *-un-lft-identity0.2
  \[\leadsto \frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - \frac{y \cdot y}{\sqrt{\color{blue}{1 \cdot \left(x \cdot x + y \cdot y\right)}}}}{\sqrt{x \cdot x + y \cdot y}}\]
8. Applied sqrt-prod0.2
  \[\leadsto \frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - \frac{y \cdot y}{\color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + y \cdot y}}}}{\sqrt{x \cdot x + y \cdot y}}\]
9. Applied times-frac0.4
  \[\leadsto \frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - \color{blue}{\frac{y}{\sqrt{1}} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}}{\sqrt{x \cdot x + y \cdot y}}\]
10. Simplified0.4
  \[\leadsto \frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - \color{blue}{y} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\]
if -1.3292537611752237e-158 < y < 7.961862811311691e-164
1. Initial program 29.2
  \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
2. Taylor expanded around inf 15.0
  \[\leadsto \color{blue}{1}\]
Recombined 3 regimes into one program.
Final simplification5.0
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -5.797856225877881060769082412965027708037 \cdot 10^{150}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -1.329253761175223739159446383274506990081 \cdot 10^{-158}:\\ \;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\ \mathbf{elif}\;y \le 7.961862811311691246218405838467989119993 \cdot 10^{-164}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{x \cdot x}{\sqrt{x \cdot x + y \cdot y}} - y \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}{\sqrt{x \cdot x + y \cdot y}}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y < -5.797856225877881e+150`

`if -5.797856225877881e+150 < y < -1.3292537611752237e-158 or 7.961862811311691e-164 < y`

`if -1.3292537611752237e-158 < y < 7.961862811311691e-164`

Reproduce

In
Out