Kahan p9 Example

Percentage Accurate: 67.6% → 92.9%
Time: 6.8s
Alternatives: 7
Speedup: 0.5×

Specification

?
\[\left(0 < x \land x < 1\right) \land y < 1\]
\[\begin{array}{l} \\ \frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \end{array} \]
(FPCore (x y) :precision binary64 (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))
double code(double x, double y) {
	return ((x - y) * (x + y)) / ((x * x) + (y * y));
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = ((x - y) * (x + y)) / ((x * x) + (y * y))
end function
public static double code(double x, double y) {
	return ((x - y) * (x + y)) / ((x * x) + (y * y));
}
def code(x, y):
	return ((x - y) * (x + y)) / ((x * x) + (y * y))
function code(x, y)
	return Float64(Float64(Float64(x - y) * Float64(x + y)) / Float64(Float64(x * x) + Float64(y * y)))
end
function tmp = code(x, y)
	tmp = ((x - y) * (x + y)) / ((x * x) + (y * y));
end
code[x_, y_] := N[(N[(N[(x - y), $MachinePrecision] * N[(x + y), $MachinePrecision]), $MachinePrecision] / N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}
\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 7 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: 67.6% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \end{array} \]
(FPCore (x y) :precision binary64 (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))
double code(double x, double y) {
	return ((x - y) * (x + y)) / ((x * x) + (y * y));
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = ((x - y) * (x + y)) / ((x * x) + (y * y))
end function
public static double code(double x, double y) {
	return ((x - y) * (x + y)) / ((x * x) + (y * y));
}
def code(x, y):
	return ((x - y) * (x + y)) / ((x * x) + (y * y))
function code(x, y)
	return Float64(Float64(Float64(x - y) * Float64(x + y)) / Float64(Float64(x * x) + Float64(y * y)))
end
function tmp = code(x, y)
	tmp = ((x - y) * (x + y)) / ((x * x) + (y * y));
end
code[x_, y_] := N[(N[(N[(x - y), $MachinePrecision] * N[(x + y), $MachinePrecision]), $MachinePrecision] / N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

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

Alternative 1: 92.9% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left(y + x\right) \cdot \left(x - y\right)\\ \mathbf{if}\;\frac{t\_0}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;\frac{t\_0}{\mathsf{fma}\left(x, x, y \cdot y\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (let* ((t_0 (* (+ y x) (- x y))))
   (if (<= (/ t_0 (+ (* y y) (* x x))) 2.0)
     (/ t_0 (fma x x (* y y)))
     (fma (/ 2.0 y) (* (/ x y) x) -1.0))))
double code(double x, double y) {
	double t_0 = (y + x) * (x - y);
	double tmp;
	if ((t_0 / ((y * y) + (x * x))) <= 2.0) {
		tmp = t_0 / fma(x, x, (y * y));
	} else {
		tmp = fma((2.0 / y), ((x / y) * x), -1.0);
	}
	return tmp;
}
function code(x, y)
	t_0 = Float64(Float64(y + x) * Float64(x - y))
	tmp = 0.0
	if (Float64(t_0 / Float64(Float64(y * y) + Float64(x * x))) <= 2.0)
		tmp = Float64(t_0 / fma(x, x, Float64(y * y)));
	else
		tmp = fma(Float64(2.0 / y), Float64(Float64(x / y) * x), -1.0);
	end
	return tmp
end
code[x_, y_] := Block[{t$95$0 = N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(t$95$0 / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 2.0], N[(t$95$0 / N[(x * x + N[(y * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(2.0 / y), $MachinePrecision] * N[(N[(x / y), $MachinePrecision] * x), $MachinePrecision] + -1.0), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \left(y + x\right) \cdot \left(x - y\right)\\
\mathbf{if}\;\frac{t\_0}{y \cdot y + x \cdot x} \leq 2:\\
\;\;\;\;\frac{t\_0}{\mathsf{fma}\left(x, x, y \cdot y\right)}\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

    1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\color{blue}{x \cdot x + y \cdot y}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\color{blue}{x \cdot x} + y \cdot y} \]
      3. lower-fma.f64100.0

        \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}} \]
    4. Applied rewrites100.0%

      \[\leadsto \frac{\left(x - y\right) \cdot \left(x + y\right)}{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}} \]

    if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

    1. Initial program 0.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
    4. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
      2. associate-+r+N/A

        \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{x}{y} + \frac{x}{y}\right) + \frac{{x}^{2}}{{y}^{2}}\right)} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      3. distribute-lft1-inN/A

        \[\leadsto \left(\color{blue}{\left(-1 + 1\right) \cdot \frac{x}{y}} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      4. metadata-evalN/A

        \[\leadsto \left(\color{blue}{0} \cdot \frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      5. mul0-lftN/A

        \[\leadsto \left(\color{blue}{0} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      6. +-lft-identityN/A

        \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}}} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      7. associate--r+N/A

        \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
      8. associate-*r/N/A

        \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
      9. div-subN/A

        \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
      10. cancel-sign-sub-invN/A

        \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      11. metadata-evalN/A

        \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      12. distribute-rgt1-inN/A

        \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      13. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      14. associate-*r/N/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
    5. Applied rewrites85.6%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification95.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{\mathsf{fma}\left(x, x, y \cdot y\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 91.6% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\ \mathbf{if}\;t\_0 \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;t\_0 \leq 2:\\ \;\;\;\;\mathsf{fma}\left(\frac{-2}{x}, \frac{y}{x} \cdot y, 1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (let* ((t_0 (/ (* (+ y x) (- x y)) (+ (* y y) (* x x)))))
   (if (<= t_0 -0.5)
     (fma (* (/ 2.0 (* y y)) x) x -1.0)
     (if (<= t_0 2.0)
       (fma (/ -2.0 x) (* (/ y x) y) 1.0)
       (fma (/ 2.0 y) (* (/ x y) x) -1.0)))))
double code(double x, double y) {
	double t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
	double tmp;
	if (t_0 <= -0.5) {
		tmp = fma(((2.0 / (y * y)) * x), x, -1.0);
	} else if (t_0 <= 2.0) {
		tmp = fma((-2.0 / x), ((y / x) * y), 1.0);
	} else {
		tmp = fma((2.0 / y), ((x / y) * x), -1.0);
	}
	return tmp;
}
function code(x, y)
	t_0 = Float64(Float64(Float64(y + x) * Float64(x - y)) / Float64(Float64(y * y) + Float64(x * x)))
	tmp = 0.0
	if (t_0 <= -0.5)
		tmp = fma(Float64(Float64(2.0 / Float64(y * y)) * x), x, -1.0);
	elseif (t_0 <= 2.0)
		tmp = fma(Float64(-2.0 / x), Float64(Float64(y / x) * y), 1.0);
	else
		tmp = fma(Float64(2.0 / y), Float64(Float64(x / y) * x), -1.0);
	end
	return tmp
end
code[x_, y_] := Block[{t$95$0 = N[(N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision] / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$0, -0.5], N[(N[(N[(2.0 / N[(y * y), $MachinePrecision]), $MachinePrecision] * x), $MachinePrecision] * x + -1.0), $MachinePrecision], If[LessEqual[t$95$0, 2.0], N[(N[(-2.0 / x), $MachinePrecision] * N[(N[(y / x), $MachinePrecision] * y), $MachinePrecision] + 1.0), $MachinePrecision], N[(N[(2.0 / y), $MachinePrecision] * N[(N[(x / y), $MachinePrecision] * x), $MachinePrecision] + -1.0), $MachinePrecision]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\
\mathbf{if}\;t\_0 \leq -0.5:\\
\;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\

\mathbf{elif}\;t\_0 \leq 2:\\
\;\;\;\;\mathsf{fma}\left(\frac{-2}{x}, \frac{y}{x} \cdot y, 1\right)\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < -0.5

    1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\left(x - y\right) \cdot \left(x + y\right)}}{x \cdot x + y \cdot y} \]
      3. associate-/l*N/A

        \[\leadsto \color{blue}{\left(x - y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}} \]
      4. lift--.f64N/A

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      5. flip--N/A

        \[\leadsto \color{blue}{\frac{x \cdot x - y \cdot y}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      6. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{x \cdot x} - y \cdot y}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      7. lift-*.f64N/A

        \[\leadsto \frac{x \cdot x - \color{blue}{y \cdot y}}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      8. lift-+.f64N/A

        \[\leadsto \frac{x \cdot x - y \cdot y}{\color{blue}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      9. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
      10. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
    4. Applied rewrites99.7%

      \[\leadsto \color{blue}{\frac{\frac{y + x}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \mathsf{fma}\left(-y, y, x \cdot x\right)}{y + x}} \]
    5. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}} - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
    6. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \frac{{x}^{2}}{{y}^{2}} - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
      2. associate--r+N/A

        \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
      3. associate-*r/N/A

        \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
      4. div-subN/A

        \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
      5. cancel-sign-sub-invN/A

        \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      6. metadata-evalN/A

        \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      7. distribute-rgt1-inN/A

        \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      8. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      9. associate-*r/N/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
      10. sub-negN/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}} + \left(\mathsf{neg}\left(1\right)\right)} \]
      11. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{2 \cdot {x}^{2}}{{y}^{2}}} + \left(\mathsf{neg}\left(1\right)\right) \]
      12. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{2}{{y}^{2}} \cdot {x}^{2}} + \left(\mathsf{neg}\left(1\right)\right) \]
      13. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2 \cdot 1}}{{y}^{2}} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
      14. associate-*r/N/A

        \[\leadsto \color{blue}{\left(2 \cdot \frac{1}{{y}^{2}}\right)} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
      15. unpow2N/A

        \[\leadsto \left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot \color{blue}{\left(x \cdot x\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
      16. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x} + \left(\mathsf{neg}\left(1\right)\right) \]
      17. metadata-evalN/A

        \[\leadsto \left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x + \color{blue}{-1} \]
    7. Applied rewrites98.7%

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

    if -0.5 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

    1. Initial program 99.9%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\left(x - y\right) \cdot \left(x + y\right)}}{x \cdot x + y \cdot y} \]
      3. associate-/l*N/A

        \[\leadsto \color{blue}{\left(x - y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}} \]
      4. lift--.f64N/A

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      5. flip--N/A

        \[\leadsto \color{blue}{\frac{x \cdot x - y \cdot y}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      6. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{x \cdot x} - y \cdot y}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      7. lift-*.f64N/A

        \[\leadsto \frac{x \cdot x - \color{blue}{y \cdot y}}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      8. lift-+.f64N/A

        \[\leadsto \frac{x \cdot x - y \cdot y}{\color{blue}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      9. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
      10. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
    4. Applied rewrites99.7%

      \[\leadsto \color{blue}{\frac{\frac{y + x}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \mathsf{fma}\left(-y, y, x \cdot x\right)}{y + x}} \]
    5. Taylor expanded in y around 0

      \[\leadsto \color{blue}{1 + -2 \cdot \frac{{y}^{2}}{{x}^{2}}} \]
    6. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \color{blue}{-2 \cdot \frac{{y}^{2}}{{x}^{2}} + 1} \]
      2. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{-2 \cdot {y}^{2}}{{x}^{2}}} + 1 \]
      3. unpow2N/A

        \[\leadsto \frac{-2 \cdot {y}^{2}}{\color{blue}{x \cdot x}} + 1 \]
      4. times-fracN/A

        \[\leadsto \color{blue}{\frac{-2}{x} \cdot \frac{{y}^{2}}{x}} + 1 \]
      5. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(2\right)}}{x} \cdot \frac{{y}^{2}}{x} + 1 \]
      6. distribute-neg-fracN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\frac{2}{x}\right)\right)} \cdot \frac{{y}^{2}}{x} + 1 \]
      7. metadata-evalN/A

        \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{2 \cdot 1}}{x}\right)\right) \cdot \frac{{y}^{2}}{x} + 1 \]
      8. associate-*r/N/A

        \[\leadsto \left(\mathsf{neg}\left(\color{blue}{2 \cdot \frac{1}{x}}\right)\right) \cdot \frac{{y}^{2}}{x} + 1 \]
      9. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(2 \cdot \frac{1}{x}\right), \frac{{y}^{2}}{x}, 1\right)} \]
      10. associate-*r/N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\color{blue}{\frac{2 \cdot 1}{x}}\right), \frac{{y}^{2}}{x}, 1\right) \]
      11. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\mathsf{neg}\left(\frac{\color{blue}{2}}{x}\right), \frac{{y}^{2}}{x}, 1\right) \]
      12. distribute-neg-fracN/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{\mathsf{neg}\left(2\right)}{x}}, \frac{{y}^{2}}{x}, 1\right) \]
      13. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\frac{\color{blue}{-2}}{x}, \frac{{y}^{2}}{x}, 1\right) \]
      14. lower-/.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{-2}{x}}, \frac{{y}^{2}}{x}, 1\right) \]
      15. unpow2N/A

        \[\leadsto \mathsf{fma}\left(\frac{-2}{x}, \frac{\color{blue}{y \cdot y}}{x}, 1\right) \]
      16. associate-/l*N/A

        \[\leadsto \mathsf{fma}\left(\frac{-2}{x}, \color{blue}{y \cdot \frac{y}{x}}, 1\right) \]
      17. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{-2}{x}, \color{blue}{y \cdot \frac{y}{x}}, 1\right) \]
      18. lower-/.f6499.8

        \[\leadsto \mathsf{fma}\left(\frac{-2}{x}, y \cdot \color{blue}{\frac{y}{x}}, 1\right) \]
    7. Applied rewrites99.8%

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

    if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

    1. Initial program 0.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
    4. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
      2. associate-+r+N/A

        \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{x}{y} + \frac{x}{y}\right) + \frac{{x}^{2}}{{y}^{2}}\right)} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      3. distribute-lft1-inN/A

        \[\leadsto \left(\color{blue}{\left(-1 + 1\right) \cdot \frac{x}{y}} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      4. metadata-evalN/A

        \[\leadsto \left(\color{blue}{0} \cdot \frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      5. mul0-lftN/A

        \[\leadsto \left(\color{blue}{0} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      6. +-lft-identityN/A

        \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}}} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
      7. associate--r+N/A

        \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
      8. associate-*r/N/A

        \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
      9. div-subN/A

        \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
      10. cancel-sign-sub-invN/A

        \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      11. metadata-evalN/A

        \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      12. distribute-rgt1-inN/A

        \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      13. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      14. associate-*r/N/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
    5. Applied rewrites85.6%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification95.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;\mathsf{fma}\left(\frac{-2}{x}, \frac{y}{x} \cdot y, 1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 91.4% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\ \mathbf{if}\;t\_0 \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;t\_0 \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (let* ((t_0 (/ (* (+ y x) (- x y)) (+ (* y y) (* x x)))))
   (if (<= t_0 -0.5)
     (fma (* (/ 2.0 (* y y)) x) x -1.0)
     (if (<= t_0 2.0) 1.0 (fma (/ 2.0 y) (* (/ x y) x) -1.0)))))
double code(double x, double y) {
	double t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
	double tmp;
	if (t_0 <= -0.5) {
		tmp = fma(((2.0 / (y * y)) * x), x, -1.0);
	} else if (t_0 <= 2.0) {
		tmp = 1.0;
	} else {
		tmp = fma((2.0 / y), ((x / y) * x), -1.0);
	}
	return tmp;
}
function code(x, y)
	t_0 = Float64(Float64(Float64(y + x) * Float64(x - y)) / Float64(Float64(y * y) + Float64(x * x)))
	tmp = 0.0
	if (t_0 <= -0.5)
		tmp = fma(Float64(Float64(2.0 / Float64(y * y)) * x), x, -1.0);
	elseif (t_0 <= 2.0)
		tmp = 1.0;
	else
		tmp = fma(Float64(2.0 / y), Float64(Float64(x / y) * x), -1.0);
	end
	return tmp
end
code[x_, y_] := Block[{t$95$0 = N[(N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision] / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$0, -0.5], N[(N[(N[(2.0 / N[(y * y), $MachinePrecision]), $MachinePrecision] * x), $MachinePrecision] * x + -1.0), $MachinePrecision], If[LessEqual[t$95$0, 2.0], 1.0, N[(N[(2.0 / y), $MachinePrecision] * N[(N[(x / y), $MachinePrecision] * x), $MachinePrecision] + -1.0), $MachinePrecision]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\
\mathbf{if}\;t\_0 \leq -0.5:\\
\;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\

\mathbf{elif}\;t\_0 \leq 2:\\
\;\;\;\;1\\

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


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < -0.5

    1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\left(x - y\right) \cdot \left(x + y\right)}}{x \cdot x + y \cdot y} \]
      3. associate-/l*N/A

        \[\leadsto \color{blue}{\left(x - y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}} \]
      4. lift--.f64N/A

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      5. flip--N/A

        \[\leadsto \color{blue}{\frac{x \cdot x - y \cdot y}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      6. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{x \cdot x} - y \cdot y}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      7. lift-*.f64N/A

        \[\leadsto \frac{x \cdot x - \color{blue}{y \cdot y}}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      8. lift-+.f64N/A

        \[\leadsto \frac{x \cdot x - y \cdot y}{\color{blue}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
      9. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
      10. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
    4. Applied rewrites99.7%

      \[\leadsto \color{blue}{\frac{\frac{y + x}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \mathsf{fma}\left(-y, y, x \cdot x\right)}{y + x}} \]
    5. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}} - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
    6. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \frac{{x}^{2}}{{y}^{2}} - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
      2. associate--r+N/A

        \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
      3. associate-*r/N/A

        \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
      4. div-subN/A

        \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
      5. cancel-sign-sub-invN/A

        \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      6. metadata-evalN/A

        \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      7. distribute-rgt1-inN/A

        \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
      8. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
      9. associate-*r/N/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
      10. sub-negN/A

        \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}} + \left(\mathsf{neg}\left(1\right)\right)} \]
      11. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{2 \cdot {x}^{2}}{{y}^{2}}} + \left(\mathsf{neg}\left(1\right)\right) \]
      12. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{2}{{y}^{2}} \cdot {x}^{2}} + \left(\mathsf{neg}\left(1\right)\right) \]
      13. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{2 \cdot 1}}{{y}^{2}} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
      14. associate-*r/N/A

        \[\leadsto \color{blue}{\left(2 \cdot \frac{1}{{y}^{2}}\right)} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
      15. unpow2N/A

        \[\leadsto \left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot \color{blue}{\left(x \cdot x\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
      16. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x} + \left(\mathsf{neg}\left(1\right)\right) \]
      17. metadata-evalN/A

        \[\leadsto \left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x + \color{blue}{-1} \]
    7. Applied rewrites98.7%

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

    if -0.5 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

    1. Initial program 99.9%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
    2. Add Preprocessing
    3. Taylor expanded in y around 0

      \[\leadsto \color{blue}{1} \]
    4. Step-by-step derivation
      1. Applied rewrites98.4%

        \[\leadsto \color{blue}{1} \]

      if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

      1. Initial program 0.0%

        \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
      2. Add Preprocessing
      3. Taylor expanded in y around inf

        \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
      4. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
        2. associate-+r+N/A

          \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{x}{y} + \frac{x}{y}\right) + \frac{{x}^{2}}{{y}^{2}}\right)} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
        3. distribute-lft1-inN/A

          \[\leadsto \left(\color{blue}{\left(-1 + 1\right) \cdot \frac{x}{y}} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
        4. metadata-evalN/A

          \[\leadsto \left(\color{blue}{0} \cdot \frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
        5. mul0-lftN/A

          \[\leadsto \left(\color{blue}{0} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
        6. +-lft-identityN/A

          \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}}} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
        7. associate--r+N/A

          \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
        8. associate-*r/N/A

          \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
        9. div-subN/A

          \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
        10. cancel-sign-sub-invN/A

          \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
        11. metadata-evalN/A

          \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
        12. distribute-rgt1-inN/A

          \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
        13. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
        14. associate-*r/N/A

          \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
      5. Applied rewrites85.6%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)} \]
    5. Recombined 3 regimes into one program.
    6. Final simplification94.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \]
    7. Add Preprocessing

    Alternative 4: 90.8% accurate, 0.4× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\ \mathbf{if}\;t\_0 \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;t\_0 \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-1\\ \end{array} \end{array} \]
    (FPCore (x y)
     :precision binary64
     (let* ((t_0 (/ (* (+ y x) (- x y)) (+ (* y y) (* x x)))))
       (if (<= t_0 -0.5)
         (fma (* (/ 2.0 (* y y)) x) x -1.0)
         (if (<= t_0 2.0) 1.0 -1.0))))
    double code(double x, double y) {
    	double t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
    	double tmp;
    	if (t_0 <= -0.5) {
    		tmp = fma(((2.0 / (y * y)) * x), x, -1.0);
    	} else if (t_0 <= 2.0) {
    		tmp = 1.0;
    	} else {
    		tmp = -1.0;
    	}
    	return tmp;
    }
    
    function code(x, y)
    	t_0 = Float64(Float64(Float64(y + x) * Float64(x - y)) / Float64(Float64(y * y) + Float64(x * x)))
    	tmp = 0.0
    	if (t_0 <= -0.5)
    		tmp = fma(Float64(Float64(2.0 / Float64(y * y)) * x), x, -1.0);
    	elseif (t_0 <= 2.0)
    		tmp = 1.0;
    	else
    		tmp = -1.0;
    	end
    	return tmp
    end
    
    code[x_, y_] := Block[{t$95$0 = N[(N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision] / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$0, -0.5], N[(N[(N[(2.0 / N[(y * y), $MachinePrecision]), $MachinePrecision] * x), $MachinePrecision] * x + -1.0), $MachinePrecision], If[LessEqual[t$95$0, 2.0], 1.0, -1.0]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\
    \mathbf{if}\;t\_0 \leq -0.5:\\
    \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\
    
    \mathbf{elif}\;t\_0 \leq 2:\\
    \;\;\;\;1\\
    
    \mathbf{else}:\\
    \;\;\;\;-1\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < -0.5

      1. Initial program 100.0%

        \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x - y\right) \cdot \left(x + y\right)}}{x \cdot x + y \cdot y} \]
        3. associate-/l*N/A

          \[\leadsto \color{blue}{\left(x - y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}} \]
        4. lift--.f64N/A

          \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
        5. flip--N/A

          \[\leadsto \color{blue}{\frac{x \cdot x - y \cdot y}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
        6. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{x \cdot x} - y \cdot y}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
        7. lift-*.f64N/A

          \[\leadsto \frac{x \cdot x - \color{blue}{y \cdot y}}{x + y} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
        8. lift-+.f64N/A

          \[\leadsto \frac{x \cdot x - y \cdot y}{\color{blue}{x + y}} \cdot \frac{x + y}{x \cdot x + y \cdot y} \]
        9. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
        10. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left(x \cdot x - y \cdot y\right) \cdot \frac{x + y}{x \cdot x + y \cdot y}}{x + y}} \]
      4. Applied rewrites99.7%

        \[\leadsto \color{blue}{\frac{\frac{y + x}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \mathsf{fma}\left(-y, y, x \cdot x\right)}{y + x}} \]
      5. Taylor expanded in y around inf

        \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}} - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \frac{{x}^{2}}{{y}^{2}} - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
        2. associate--r+N/A

          \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
        3. associate-*r/N/A

          \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
        4. div-subN/A

          \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
        5. cancel-sign-sub-invN/A

          \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
        6. metadata-evalN/A

          \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
        7. distribute-rgt1-inN/A

          \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
        8. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
        9. associate-*r/N/A

          \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
        10. sub-negN/A

          \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}} + \left(\mathsf{neg}\left(1\right)\right)} \]
        11. associate-*r/N/A

          \[\leadsto \color{blue}{\frac{2 \cdot {x}^{2}}{{y}^{2}}} + \left(\mathsf{neg}\left(1\right)\right) \]
        12. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{2}{{y}^{2}} \cdot {x}^{2}} + \left(\mathsf{neg}\left(1\right)\right) \]
        13. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{2 \cdot 1}}{{y}^{2}} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
        14. associate-*r/N/A

          \[\leadsto \color{blue}{\left(2 \cdot \frac{1}{{y}^{2}}\right)} \cdot {x}^{2} + \left(\mathsf{neg}\left(1\right)\right) \]
        15. unpow2N/A

          \[\leadsto \left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot \color{blue}{\left(x \cdot x\right)} + \left(\mathsf{neg}\left(1\right)\right) \]
        16. associate-*r*N/A

          \[\leadsto \color{blue}{\left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x} + \left(\mathsf{neg}\left(1\right)\right) \]
        17. metadata-evalN/A

          \[\leadsto \left(\left(2 \cdot \frac{1}{{y}^{2}}\right) \cdot x\right) \cdot x + \color{blue}{-1} \]
      7. Applied rewrites98.7%

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

      if -0.5 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

      1. Initial program 99.9%

        \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
      2. Add Preprocessing
      3. Taylor expanded in y around 0

        \[\leadsto \color{blue}{1} \]
      4. Step-by-step derivation
        1. Applied rewrites98.4%

          \[\leadsto \color{blue}{1} \]

        if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

        1. Initial program 0.0%

          \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
        2. Add Preprocessing
        3. Taylor expanded in y around inf

          \[\leadsto \color{blue}{-1} \]
        4. Step-by-step derivation
          1. Applied rewrites83.7%

            \[\leadsto \color{blue}{-1} \]
        5. Recombined 3 regimes into one program.
        6. Final simplification94.3%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq -0.5:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y \cdot y} \cdot x, x, -1\right)\\ \mathbf{elif}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-1\\ \end{array} \]
        7. Add Preprocessing

        Alternative 5: 91.5% accurate, 0.4× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\ \mathbf{if}\;t\_0 \leq -0.5:\\ \;\;\;\;-1\\ \mathbf{elif}\;t\_0 \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-1\\ \end{array} \end{array} \]
        (FPCore (x y)
         :precision binary64
         (let* ((t_0 (/ (* (+ y x) (- x y)) (+ (* y y) (* x x)))))
           (if (<= t_0 -0.5) -1.0 (if (<= t_0 2.0) 1.0 -1.0))))
        double code(double x, double y) {
        	double t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
        	double tmp;
        	if (t_0 <= -0.5) {
        		tmp = -1.0;
        	} else if (t_0 <= 2.0) {
        		tmp = 1.0;
        	} else {
        		tmp = -1.0;
        	}
        	return tmp;
        }
        
        real(8) function code(x, y)
            real(8), intent (in) :: x
            real(8), intent (in) :: y
            real(8) :: t_0
            real(8) :: tmp
            t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x))
            if (t_0 <= (-0.5d0)) then
                tmp = -1.0d0
            else if (t_0 <= 2.0d0) then
                tmp = 1.0d0
            else
                tmp = -1.0d0
            end if
            code = tmp
        end function
        
        public static double code(double x, double y) {
        	double t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
        	double tmp;
        	if (t_0 <= -0.5) {
        		tmp = -1.0;
        	} else if (t_0 <= 2.0) {
        		tmp = 1.0;
        	} else {
        		tmp = -1.0;
        	}
        	return tmp;
        }
        
        def code(x, y):
        	t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x))
        	tmp = 0
        	if t_0 <= -0.5:
        		tmp = -1.0
        	elif t_0 <= 2.0:
        		tmp = 1.0
        	else:
        		tmp = -1.0
        	return tmp
        
        function code(x, y)
        	t_0 = Float64(Float64(Float64(y + x) * Float64(x - y)) / Float64(Float64(y * y) + Float64(x * x)))
        	tmp = 0.0
        	if (t_0 <= -0.5)
        		tmp = -1.0;
        	elseif (t_0 <= 2.0)
        		tmp = 1.0;
        	else
        		tmp = -1.0;
        	end
        	return tmp
        end
        
        function tmp_2 = code(x, y)
        	t_0 = ((y + x) * (x - y)) / ((y * y) + (x * x));
        	tmp = 0.0;
        	if (t_0 <= -0.5)
        		tmp = -1.0;
        	elseif (t_0 <= 2.0)
        		tmp = 1.0;
        	else
        		tmp = -1.0;
        	end
        	tmp_2 = tmp;
        end
        
        code[x_, y_] := Block[{t$95$0 = N[(N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision] / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$0, -0.5], -1.0, If[LessEqual[t$95$0, 2.0], 1.0, -1.0]]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_0 := \frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x}\\
        \mathbf{if}\;t\_0 \leq -0.5:\\
        \;\;\;\;-1\\
        
        \mathbf{elif}\;t\_0 \leq 2:\\
        \;\;\;\;1\\
        
        \mathbf{else}:\\
        \;\;\;\;-1\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < -0.5 or 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

          1. Initial program 59.4%

            \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
          2. Add Preprocessing
          3. Taylor expanded in y around inf

            \[\leadsto \color{blue}{-1} \]
          4. Step-by-step derivation
            1. Applied rewrites92.3%

              \[\leadsto \color{blue}{-1} \]

            if -0.5 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

            1. Initial program 99.9%

              \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
            2. Add Preprocessing
            3. Taylor expanded in y around 0

              \[\leadsto \color{blue}{1} \]
            4. Step-by-step derivation
              1. Applied rewrites98.4%

                \[\leadsto \color{blue}{1} \]
            5. Recombined 2 regimes into one program.
            6. Final simplification94.1%

              \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq -0.5:\\ \;\;\;\;-1\\ \mathbf{elif}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-1\\ \end{array} \]
            7. Add Preprocessing

            Alternative 6: 92.1% accurate, 0.5× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;\left(y + x\right) \cdot \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \end{array} \]
            (FPCore (x y)
             :precision binary64
             (if (<= (/ (* (+ y x) (- x y)) (+ (* y y) (* x x))) 2.0)
               (* (+ y x) (/ (- x y) (fma y y (* x x))))
               (fma (/ 2.0 y) (* (/ x y) x) -1.0)))
            double code(double x, double y) {
            	double tmp;
            	if ((((y + x) * (x - y)) / ((y * y) + (x * x))) <= 2.0) {
            		tmp = (y + x) * ((x - y) / fma(y, y, (x * x)));
            	} else {
            		tmp = fma((2.0 / y), ((x / y) * x), -1.0);
            	}
            	return tmp;
            }
            
            function code(x, y)
            	tmp = 0.0
            	if (Float64(Float64(Float64(y + x) * Float64(x - y)) / Float64(Float64(y * y) + Float64(x * x))) <= 2.0)
            		tmp = Float64(Float64(y + x) * Float64(Float64(x - y) / fma(y, y, Float64(x * x))));
            	else
            		tmp = fma(Float64(2.0 / y), Float64(Float64(x / y) * x), -1.0);
            	end
            	return tmp
            end
            
            code[x_, y_] := If[LessEqual[N[(N[(N[(y + x), $MachinePrecision] * N[(x - y), $MachinePrecision]), $MachinePrecision] / N[(N[(y * y), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 2.0], N[(N[(y + x), $MachinePrecision] * N[(N[(x - y), $MachinePrecision] / N[(y * y + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(2.0 / y), $MachinePrecision] * N[(N[(x / y), $MachinePrecision] * x), $MachinePrecision] + -1.0), $MachinePrecision]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\
            \;\;\;\;\left(y + x\right) \cdot \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)}\\
            
            \mathbf{else}:\\
            \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

              1. Initial program 100.0%

                \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
              2. Add Preprocessing
              3. Step-by-step derivation
                1. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}} \]
                2. lift-*.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x - y\right) \cdot \left(x + y\right)}}{x \cdot x + y \cdot y} \]
                3. *-commutativeN/A

                  \[\leadsto \frac{\color{blue}{\left(x + y\right) \cdot \left(x - y\right)}}{x \cdot x + y \cdot y} \]
                4. associate-/l*N/A

                  \[\leadsto \color{blue}{\left(x + y\right) \cdot \frac{x - y}{x \cdot x + y \cdot y}} \]
                5. *-commutativeN/A

                  \[\leadsto \color{blue}{\frac{x - y}{x \cdot x + y \cdot y} \cdot \left(x + y\right)} \]
                6. lower-*.f64N/A

                  \[\leadsto \color{blue}{\frac{x - y}{x \cdot x + y \cdot y} \cdot \left(x + y\right)} \]
                7. lower-/.f6498.6

                  \[\leadsto \color{blue}{\frac{x - y}{x \cdot x + y \cdot y}} \cdot \left(x + y\right) \]
                8. lift-+.f64N/A

                  \[\leadsto \frac{x - y}{\color{blue}{x \cdot x + y \cdot y}} \cdot \left(x + y\right) \]
                9. +-commutativeN/A

                  \[\leadsto \frac{x - y}{\color{blue}{y \cdot y + x \cdot x}} \cdot \left(x + y\right) \]
                10. lift-*.f64N/A

                  \[\leadsto \frac{x - y}{\color{blue}{y \cdot y} + x \cdot x} \cdot \left(x + y\right) \]
                11. lower-fma.f6498.6

                  \[\leadsto \frac{x - y}{\color{blue}{\mathsf{fma}\left(y, y, x \cdot x\right)}} \cdot \left(x + y\right) \]
                12. lift-+.f64N/A

                  \[\leadsto \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \color{blue}{\left(x + y\right)} \]
                13. +-commutativeN/A

                  \[\leadsto \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \color{blue}{\left(y + x\right)} \]
                14. lower-+.f6498.6

                  \[\leadsto \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \color{blue}{\left(y + x\right)} \]
              4. Applied rewrites98.6%

                \[\leadsto \color{blue}{\frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)} \cdot \left(y + x\right)} \]

              if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

              1. Initial program 0.0%

                \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
              2. Add Preprocessing
              3. Taylor expanded in y around inf

                \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \left(1 + -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right)} \]
              4. Step-by-step derivation
                1. +-commutativeN/A

                  \[\leadsto \left(-1 \cdot \frac{x}{y} + \left(\frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right)\right) - \color{blue}{\left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
                2. associate-+r+N/A

                  \[\leadsto \color{blue}{\left(\left(-1 \cdot \frac{x}{y} + \frac{x}{y}\right) + \frac{{x}^{2}}{{y}^{2}}\right)} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
                3. distribute-lft1-inN/A

                  \[\leadsto \left(\color{blue}{\left(-1 + 1\right) \cdot \frac{x}{y}} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
                4. metadata-evalN/A

                  \[\leadsto \left(\color{blue}{0} \cdot \frac{x}{y} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
                5. mul0-lftN/A

                  \[\leadsto \left(\color{blue}{0} + \frac{{x}^{2}}{{y}^{2}}\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
                6. +-lft-identityN/A

                  \[\leadsto \color{blue}{\frac{{x}^{2}}{{y}^{2}}} - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right) \]
                7. associate--r+N/A

                  \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} - -1 \cdot \frac{{x}^{2}}{{y}^{2}}\right) - 1} \]
                8. associate-*r/N/A

                  \[\leadsto \left(\frac{{x}^{2}}{{y}^{2}} - \color{blue}{\frac{-1 \cdot {x}^{2}}{{y}^{2}}}\right) - 1 \]
                9. div-subN/A

                  \[\leadsto \color{blue}{\frac{{x}^{2} - -1 \cdot {x}^{2}}{{y}^{2}}} - 1 \]
                10. cancel-sign-sub-invN/A

                  \[\leadsto \frac{\color{blue}{{x}^{2} + \left(\mathsf{neg}\left(-1\right)\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
                11. metadata-evalN/A

                  \[\leadsto \frac{{x}^{2} + \color{blue}{1} \cdot {x}^{2}}{{y}^{2}} - 1 \]
                12. distribute-rgt1-inN/A

                  \[\leadsto \frac{\color{blue}{\left(1 + 1\right) \cdot {x}^{2}}}{{y}^{2}} - 1 \]
                13. metadata-evalN/A

                  \[\leadsto \frac{\color{blue}{2} \cdot {x}^{2}}{{y}^{2}} - 1 \]
                14. associate-*r/N/A

                  \[\leadsto \color{blue}{2 \cdot \frac{{x}^{2}}{{y}^{2}}} - 1 \]
              5. Applied rewrites85.6%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)} \]
            3. Recombined 2 regimes into one program.
            4. Final simplification94.9%

              \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(y + x\right) \cdot \left(x - y\right)}{y \cdot y + x \cdot x} \leq 2:\\ \;\;\;\;\left(y + x\right) \cdot \frac{x - y}{\mathsf{fma}\left(y, y, x \cdot x\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{y}, \frac{x}{y} \cdot x, -1\right)\\ \end{array} \]
            5. Add Preprocessing

            Alternative 7: 67.4% accurate, 36.0× speedup?

            \[\begin{array}{l} \\ -1 \end{array} \]
            (FPCore (x y) :precision binary64 -1.0)
            double code(double x, double y) {
            	return -1.0;
            }
            
            real(8) function code(x, y)
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                code = -1.0d0
            end function
            
            public static double code(double x, double y) {
            	return -1.0;
            }
            
            def code(x, y):
            	return -1.0
            
            function code(x, y)
            	return -1.0
            end
            
            function tmp = code(x, y)
            	tmp = -1.0;
            end
            
            code[x_, y_] := -1.0
            
            \begin{array}{l}
            
            \\
            -1
            \end{array}
            
            Derivation
            1. Initial program 71.5%

              \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
            2. Add Preprocessing
            3. Taylor expanded in y around inf

              \[\leadsto \color{blue}{-1} \]
            4. Step-by-step derivation
              1. Applied rewrites65.3%

                \[\leadsto \color{blue}{-1} \]
              2. Add Preprocessing

              Developer Target 1: 99.9% accurate, 0.4× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_0 := \left|\frac{x}{y}\right|\\ \mathbf{if}\;0.5 < t\_0 \land t\_0 < 2:\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\ \end{array} \end{array} \]
              (FPCore (x y)
               :precision binary64
               (let* ((t_0 (fabs (/ x y))))
                 (if (and (< 0.5 t_0) (< t_0 2.0))
                   (/ (* (- x y) (+ x y)) (+ (* x x) (* y y)))
                   (- 1.0 (/ 2.0 (+ 1.0 (* (/ x y) (/ x y))))))))
              double code(double x, double y) {
              	double t_0 = fabs((x / y));
              	double tmp;
              	if ((0.5 < t_0) && (t_0 < 2.0)) {
              		tmp = ((x - y) * (x + y)) / ((x * x) + (y * y));
              	} else {
              		tmp = 1.0 - (2.0 / (1.0 + ((x / y) * (x / y))));
              	}
              	return tmp;
              }
              
              real(8) function code(x, y)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: y
                  real(8) :: t_0
                  real(8) :: tmp
                  t_0 = abs((x / y))
                  if ((0.5d0 < t_0) .and. (t_0 < 2.0d0)) then
                      tmp = ((x - y) * (x + y)) / ((x * x) + (y * y))
                  else
                      tmp = 1.0d0 - (2.0d0 / (1.0d0 + ((x / y) * (x / y))))
                  end if
                  code = tmp
              end function
              
              public static double code(double x, double y) {
              	double t_0 = Math.abs((x / y));
              	double tmp;
              	if ((0.5 < t_0) && (t_0 < 2.0)) {
              		tmp = ((x - y) * (x + y)) / ((x * x) + (y * y));
              	} else {
              		tmp = 1.0 - (2.0 / (1.0 + ((x / y) * (x / y))));
              	}
              	return tmp;
              }
              
              def code(x, y):
              	t_0 = math.fabs((x / y))
              	tmp = 0
              	if (0.5 < t_0) and (t_0 < 2.0):
              		tmp = ((x - y) * (x + y)) / ((x * x) + (y * y))
              	else:
              		tmp = 1.0 - (2.0 / (1.0 + ((x / y) * (x / y))))
              	return tmp
              
              function code(x, y)
              	t_0 = abs(Float64(x / y))
              	tmp = 0.0
              	if ((0.5 < t_0) && (t_0 < 2.0))
              		tmp = Float64(Float64(Float64(x - y) * Float64(x + y)) / Float64(Float64(x * x) + Float64(y * y)));
              	else
              		tmp = Float64(1.0 - Float64(2.0 / Float64(1.0 + Float64(Float64(x / y) * Float64(x / y)))));
              	end
              	return tmp
              end
              
              function tmp_2 = code(x, y)
              	t_0 = abs((x / y));
              	tmp = 0.0;
              	if ((0.5 < t_0) && (t_0 < 2.0))
              		tmp = ((x - y) * (x + y)) / ((x * x) + (y * y));
              	else
              		tmp = 1.0 - (2.0 / (1.0 + ((x / y) * (x / y))));
              	end
              	tmp_2 = tmp;
              end
              
              code[x_, y_] := Block[{t$95$0 = N[Abs[N[(x / y), $MachinePrecision]], $MachinePrecision]}, If[And[Less[0.5, t$95$0], Less[t$95$0, 2.0]], N[(N[(N[(x - y), $MachinePrecision] * N[(x + y), $MachinePrecision]), $MachinePrecision] / N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1.0 - N[(2.0 / N[(1.0 + N[(N[(x / y), $MachinePrecision] * N[(x / y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_0 := \left|\frac{x}{y}\right|\\
              \mathbf{if}\;0.5 < t\_0 \land t\_0 < 2:\\
              \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\
              
              \mathbf{else}:\\
              \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\
              
              
              \end{array}
              \end{array}
              

              Reproduce

              ?
              herbie shell --seed 2024255 
              (FPCore (x y)
                :name "Kahan p9 Example"
                :precision binary64
                :pre (and (and (< 0.0 x) (< x 1.0)) (< y 1.0))
              
                :alt
                (! :herbie-platform default (if (< 1/2 (fabs (/ x y)) 2) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1 (/ 2 (+ 1 (* (/ x y) (/ x y)))))))
              
                (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))