Graphics.Rendering.Chart.Plot.AreaSpots:renderSpotLegend from Chart-1.5.3

Percentage Accurate: 99.9% → 99.9%
Time: 7.8s
Alternatives: 11
Speedup: 1.7×

Specification

?
\[\begin{array}{l} \\ x + \frac{\left|y - x\right|}{2} \end{array} \]
(FPCore (x y) :precision binary64 (+ x (/ (fabs (- y x)) 2.0)))
double code(double x, double y) {
	return x + (fabs((y - x)) / 2.0);
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = x + (abs((y - x)) / 2.0d0)
end function
public static double code(double x, double y) {
	return x + (Math.abs((y - x)) / 2.0);
}
def code(x, y):
	return x + (math.fabs((y - x)) / 2.0)
function code(x, y)
	return Float64(x + Float64(abs(Float64(y - x)) / 2.0))
end
function tmp = code(x, y)
	tmp = x + (abs((y - x)) / 2.0);
end
code[x_, y_] := N[(x + N[(N[Abs[N[(y - x), $MachinePrecision]], $MachinePrecision] / 2.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
x + \frac{\left|y - x\right|}{2}
\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 11 alternatives:

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

Initial Program: 99.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ x + \frac{\left|y - x\right|}{2} \end{array} \]
(FPCore (x y) :precision binary64 (+ x (/ (fabs (- y x)) 2.0)))
double code(double x, double y) {
	return x + (fabs((y - x)) / 2.0);
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    code = x + (abs((y - x)) / 2.0d0)
end function
public static double code(double x, double y) {
	return x + (Math.abs((y - x)) / 2.0);
}
def code(x, y):
	return x + (math.fabs((y - x)) / 2.0)
function code(x, y)
	return Float64(x + Float64(abs(Float64(y - x)) / 2.0))
end
function tmp = code(x, y)
	tmp = x + (abs((y - x)) / 2.0);
end
code[x_, y_] := N[(x + N[(N[Abs[N[(y - x), $MachinePrecision]], $MachinePrecision] / 2.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
x + \frac{\left|y - x\right|}{2}
\end{array}

Alternative 1: 99.9% accurate, 1.7× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(\left|y - x\right|, 0.5, x\right) \end{array} \]
(FPCore (x y) :precision binary64 (fma (fabs (- y x)) 0.5 x))
double code(double x, double y) {
	return fma(fabs((y - x)), 0.5, x);
}
function code(x, y)
	return fma(abs(Float64(y - x)), 0.5, x)
end
code[x_, y_] := N[(N[Abs[N[(y - x), $MachinePrecision]], $MachinePrecision] * 0.5 + x), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(\left|y - x\right|, 0.5, x\right)
\end{array}
Derivation
  1. Initial program 99.9%

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

      \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
    2. +-commutativeN/A

      \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
    3. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
    4. div-invN/A

      \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
    5. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
    6. lift-fabs.f64N/A

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
    7. neg-fabsN/A

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

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
    9. lift--.f64N/A

      \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
    10. sub-negN/A

      \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
    11. +-commutativeN/A

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

      \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
    13. remove-double-negN/A

      \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
    14. sub-negN/A

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

      \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
    16. metadata-eval99.9

      \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
  4. Applied rewrites99.9%

    \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
  5. Final simplification99.9%

    \[\leadsto \mathsf{fma}\left(\left|y - x\right|, 0.5, x\right) \]
  6. Add Preprocessing

Alternative 2: 49.9% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\left|y - x\right|}{2} + x \leq 4 \cdot 10^{-240}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (if (<= (+ (/ (fabs (- y x)) 2.0) x) 4e-240) (* 0.5 x) (* 0.5 y)))
double code(double x, double y) {
	double tmp;
	if (((fabs((y - x)) / 2.0) + x) <= 4e-240) {
		tmp = 0.5 * x;
	} else {
		tmp = 0.5 * y;
	}
	return tmp;
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8) :: tmp
    if (((abs((y - x)) / 2.0d0) + x) <= 4d-240) then
        tmp = 0.5d0 * x
    else
        tmp = 0.5d0 * y
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double tmp;
	if (((Math.abs((y - x)) / 2.0) + x) <= 4e-240) {
		tmp = 0.5 * x;
	} else {
		tmp = 0.5 * y;
	}
	return tmp;
}
def code(x, y):
	tmp = 0
	if ((math.fabs((y - x)) / 2.0) + x) <= 4e-240:
		tmp = 0.5 * x
	else:
		tmp = 0.5 * y
	return tmp
function code(x, y)
	tmp = 0.0
	if (Float64(Float64(abs(Float64(y - x)) / 2.0) + x) <= 4e-240)
		tmp = Float64(0.5 * x);
	else
		tmp = Float64(0.5 * y);
	end
	return tmp
end
function tmp_2 = code(x, y)
	tmp = 0.0;
	if (((abs((y - x)) / 2.0) + x) <= 4e-240)
		tmp = 0.5 * x;
	else
		tmp = 0.5 * y;
	end
	tmp_2 = tmp;
end
code[x_, y_] := If[LessEqual[N[(N[(N[Abs[N[(y - x), $MachinePrecision]], $MachinePrecision] / 2.0), $MachinePrecision] + x), $MachinePrecision], 4e-240], N[(0.5 * x), $MachinePrecision], N[(0.5 * y), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\left|y - x\right|}{2} + x \leq 4 \cdot 10^{-240}:\\
\;\;\;\;0.5 \cdot x\\

\mathbf{else}:\\
\;\;\;\;0.5 \cdot y\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (+.f64 x (/.f64 (fabs.f64 (-.f64 y x)) #s(literal 2 binary64))) < 3.9999999999999999e-240

    1. Initial program 100.0%

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

        \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
      2. +-commutativeN/A

        \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
      5. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
      6. lift-fabs.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
      7. neg-fabsN/A

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
      9. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
      10. sub-negN/A

        \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
      11. +-commutativeN/A

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

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
      13. remove-double-negN/A

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
      14. sub-negN/A

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

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
      16. metadata-eval100.0

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

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
    5. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
      2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
      3. unpow2N/A

        \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
      4. rem-square-sqrtN/A

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

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

        \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
      7. lower-*.f6489.8

        \[\leadsto \color{blue}{0.5 \cdot x} \]
    9. Applied rewrites89.8%

      \[\leadsto \color{blue}{0.5 \cdot x} \]

    if 3.9999999999999999e-240 < (+.f64 x (/.f64 (fabs.f64 (-.f64 y x)) #s(literal 2 binary64)))

    1. Initial program 99.9%

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

        \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
      2. +-commutativeN/A

        \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
      5. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
      6. lift-fabs.f64N/A

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
      7. neg-fabsN/A

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

        \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
      9. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
      10. sub-negN/A

        \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
      11. +-commutativeN/A

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

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
      13. remove-double-negN/A

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
      14. sub-negN/A

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

        \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
      16. metadata-eval99.9

        \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
    4. Applied rewrites99.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
    5. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
      2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(-1 \cdot \frac{y \cdot {\left(\sqrt{\frac{1}{2}}\right)}^{2}}{x} + {\left(\sqrt{\frac{1}{2}}\right)}^{2}\right) - 1\right)\right)\right) \cdot x} \]
    9. Applied rewrites31.4%

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

      \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]
    11. Step-by-step derivation
      1. Applied rewrites32.4%

        \[\leadsto y \cdot \color{blue}{0.5} \]
    12. Recombined 2 regimes into one program.
    13. Final simplification50.1%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left|y - x\right|}{2} + x \leq 4 \cdot 10^{-240}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]
    14. Add Preprocessing

    Alternative 3: 58.1% accurate, 0.8× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.8 \cdot 10^{-129}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{elif}\;x \leq 10^{-262}:\\ \;\;\;\;-0.5 \cdot y\\ \mathbf{elif}\;x \leq 2.5 \cdot 10^{-35}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{else}:\\ \;\;\;\;1.5 \cdot x\\ \end{array} \end{array} \]
    (FPCore (x y)
     :precision binary64
     (if (<= x -2.8e-129)
       (* 0.5 x)
       (if (<= x 1e-262) (* -0.5 y) (if (<= x 2.5e-35) (* 0.5 y) (* 1.5 x)))))
    double code(double x, double y) {
    	double tmp;
    	if (x <= -2.8e-129) {
    		tmp = 0.5 * x;
    	} else if (x <= 1e-262) {
    		tmp = -0.5 * y;
    	} else if (x <= 2.5e-35) {
    		tmp = 0.5 * y;
    	} else {
    		tmp = 1.5 * x;
    	}
    	return tmp;
    }
    
    real(8) function code(x, y)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        real(8) :: tmp
        if (x <= (-2.8d-129)) then
            tmp = 0.5d0 * x
        else if (x <= 1d-262) then
            tmp = (-0.5d0) * y
        else if (x <= 2.5d-35) then
            tmp = 0.5d0 * y
        else
            tmp = 1.5d0 * x
        end if
        code = tmp
    end function
    
    public static double code(double x, double y) {
    	double tmp;
    	if (x <= -2.8e-129) {
    		tmp = 0.5 * x;
    	} else if (x <= 1e-262) {
    		tmp = -0.5 * y;
    	} else if (x <= 2.5e-35) {
    		tmp = 0.5 * y;
    	} else {
    		tmp = 1.5 * x;
    	}
    	return tmp;
    }
    
    def code(x, y):
    	tmp = 0
    	if x <= -2.8e-129:
    		tmp = 0.5 * x
    	elif x <= 1e-262:
    		tmp = -0.5 * y
    	elif x <= 2.5e-35:
    		tmp = 0.5 * y
    	else:
    		tmp = 1.5 * x
    	return tmp
    
    function code(x, y)
    	tmp = 0.0
    	if (x <= -2.8e-129)
    		tmp = Float64(0.5 * x);
    	elseif (x <= 1e-262)
    		tmp = Float64(-0.5 * y);
    	elseif (x <= 2.5e-35)
    		tmp = Float64(0.5 * y);
    	else
    		tmp = Float64(1.5 * x);
    	end
    	return tmp
    end
    
    function tmp_2 = code(x, y)
    	tmp = 0.0;
    	if (x <= -2.8e-129)
    		tmp = 0.5 * x;
    	elseif (x <= 1e-262)
    		tmp = -0.5 * y;
    	elseif (x <= 2.5e-35)
    		tmp = 0.5 * y;
    	else
    		tmp = 1.5 * x;
    	end
    	tmp_2 = tmp;
    end
    
    code[x_, y_] := If[LessEqual[x, -2.8e-129], N[(0.5 * x), $MachinePrecision], If[LessEqual[x, 1e-262], N[(-0.5 * y), $MachinePrecision], If[LessEqual[x, 2.5e-35], N[(0.5 * y), $MachinePrecision], N[(1.5 * x), $MachinePrecision]]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;x \leq -2.8 \cdot 10^{-129}:\\
    \;\;\;\;0.5 \cdot x\\
    
    \mathbf{elif}\;x \leq 10^{-262}:\\
    \;\;\;\;-0.5 \cdot y\\
    
    \mathbf{elif}\;x \leq 2.5 \cdot 10^{-35}:\\
    \;\;\;\;0.5 \cdot y\\
    
    \mathbf{else}:\\
    \;\;\;\;1.5 \cdot x\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 4 regimes
    2. if x < -2.7999999999999999e-129

      1. Initial program 100.0%

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

          \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
        2. +-commutativeN/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
        4. div-invN/A

          \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
        5. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
        6. lift-fabs.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
        7. neg-fabsN/A

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
        9. lift--.f64N/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
        10. sub-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
        11. +-commutativeN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
        13. remove-double-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
        14. sub-negN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
        16. metadata-eval100.0

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
      5. Step-by-step derivation
        1. lift-fma.f64N/A

          \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
        2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
        3. unpow2N/A

          \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
        4. rem-square-sqrtN/A

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

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

          \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
        7. lower-*.f6475.7

          \[\leadsto \color{blue}{0.5 \cdot x} \]
      9. Applied rewrites75.7%

        \[\leadsto \color{blue}{0.5 \cdot x} \]

      if -2.7999999999999999e-129 < x < 1.00000000000000001e-262

      1. Initial program 100.0%

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

          \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
        2. +-commutativeN/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
        4. div-invN/A

          \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
        5. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
        6. lift-fabs.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
        7. neg-fabsN/A

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
        9. lift--.f64N/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
        10. sub-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
        11. +-commutativeN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
        13. remove-double-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
        14. sub-negN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
        16. metadata-eval100.0

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
      5. Step-by-step derivation
        1. lift-fabs.f64N/A

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

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

          \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
        4. sqr-powN/A

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
        5. fabs-sqrN/A

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

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

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
      6. Applied rewrites59.8%

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

        \[\leadsto \color{blue}{\frac{-1}{2} \cdot y} \]
      8. Step-by-step derivation
        1. lower-*.f6456.7

          \[\leadsto \color{blue}{-0.5 \cdot y} \]
      9. Applied rewrites56.7%

        \[\leadsto \color{blue}{-0.5 \cdot y} \]

      if 1.00000000000000001e-262 < x < 2.49999999999999982e-35

      1. Initial program 100.0%

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

          \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
        2. +-commutativeN/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
        4. div-invN/A

          \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
        5. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
        6. lift-fabs.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
        7. neg-fabsN/A

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

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
        9. lift--.f64N/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
        10. sub-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
        11. +-commutativeN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
        13. remove-double-negN/A

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
        14. sub-negN/A

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
        16. metadata-eval100.0

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

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
      5. Step-by-step derivation
        1. lift-fma.f64N/A

          \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
        2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(-1 \cdot \frac{y \cdot {\left(\sqrt{\frac{1}{2}}\right)}^{2}}{x} + {\left(\sqrt{\frac{1}{2}}\right)}^{2}\right) - 1\right)\right)\right) \cdot x} \]
      9. Applied rewrites35.3%

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

        \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]
      11. Step-by-step derivation
        1. Applied rewrites48.4%

          \[\leadsto y \cdot \color{blue}{0.5} \]

        if 2.49999999999999982e-35 < x

        1. Initial program 99.8%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval99.8

            \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
        4. Applied rewrites99.8%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fabs.f64N/A

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

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

            \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
          4. sqr-powN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
          5. fabs-sqrN/A

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

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

            \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
          8. unpow188.0

            \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
        6. Applied rewrites88.0%

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

          \[\leadsto \color{blue}{x + \frac{1}{2} \cdot x} \]
        8. Step-by-step derivation
          1. distribute-rgt1-inN/A

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

            \[\leadsto \color{blue}{\frac{3}{2}} \cdot x \]
          3. lower-*.f6465.6

            \[\leadsto \color{blue}{1.5 \cdot x} \]
        9. Applied rewrites65.6%

          \[\leadsto \color{blue}{1.5 \cdot x} \]
      12. Recombined 4 regimes into one program.
      13. Final simplification64.4%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -2.8 \cdot 10^{-129}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{elif}\;x \leq 10^{-262}:\\ \;\;\;\;-0.5 \cdot y\\ \mathbf{elif}\;x \leq 2.5 \cdot 10^{-35}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{else}:\\ \;\;\;\;1.5 \cdot x\\ \end{array} \]
      14. Add Preprocessing

      Alternative 4: 84.1% accurate, 0.8× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.3 \cdot 10^{-127}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\ \;\;\;\;\mathsf{fma}\left(\left|-y\right|, 0.5, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(1.5, x, -0.5 \cdot y\right)\\ \end{array} \end{array} \]
      (FPCore (x y)
       :precision binary64
       (if (<= x -2.3e-127)
         (* (+ y x) 0.5)
         (if (<= x 4.6e-35) (fma (fabs (- y)) 0.5 x) (fma 1.5 x (* -0.5 y)))))
      double code(double x, double y) {
      	double tmp;
      	if (x <= -2.3e-127) {
      		tmp = (y + x) * 0.5;
      	} else if (x <= 4.6e-35) {
      		tmp = fma(fabs(-y), 0.5, x);
      	} else {
      		tmp = fma(1.5, x, (-0.5 * y));
      	}
      	return tmp;
      }
      
      function code(x, y)
      	tmp = 0.0
      	if (x <= -2.3e-127)
      		tmp = Float64(Float64(y + x) * 0.5);
      	elseif (x <= 4.6e-35)
      		tmp = fma(abs(Float64(-y)), 0.5, x);
      	else
      		tmp = fma(1.5, x, Float64(-0.5 * y));
      	end
      	return tmp
      end
      
      code[x_, y_] := If[LessEqual[x, -2.3e-127], N[(N[(y + x), $MachinePrecision] * 0.5), $MachinePrecision], If[LessEqual[x, 4.6e-35], N[(N[Abs[(-y)], $MachinePrecision] * 0.5 + x), $MachinePrecision], N[(1.5 * x + N[(-0.5 * y), $MachinePrecision]), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;x \leq -2.3 \cdot 10^{-127}:\\
      \;\;\;\;\left(y + x\right) \cdot 0.5\\
      
      \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\
      \;\;\;\;\mathsf{fma}\left(\left|-y\right|, 0.5, x\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(1.5, x, -0.5 \cdot y\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if x < -2.30000000000000019e-127

        1. Initial program 100.0%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval100.0

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fma.f64N/A

            \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
          2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
          3. unpow2N/A

            \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
          4. rem-square-sqrtN/A

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

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

            \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
          7. lower-*.f6475.7

            \[\leadsto \color{blue}{0.5 \cdot x} \]
        9. Applied rewrites75.7%

          \[\leadsto \color{blue}{0.5 \cdot x} \]
        10. Taylor expanded in x around -inf

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

          \[\leadsto \color{blue}{\left(y + x\right) \cdot 0.5} \]

        if -2.30000000000000019e-127 < x < 4.5999999999999998e-35

        1. Initial program 100.0%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval100.0

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

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-1 \cdot y}\right|, \frac{1}{2}, x\right) \]
        6. Step-by-step derivation
          1. mul-1-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\mathsf{neg}\left(y\right)}\right|, \frac{1}{2}, x\right) \]
          2. lower-neg.f6488.4

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-y}\right|, 0.5, x\right) \]
        7. Applied rewrites88.4%

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-y}\right|, 0.5, x\right) \]

        if 4.5999999999999998e-35 < x

        1. Initial program 99.8%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval99.8

            \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
        4. Applied rewrites99.8%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fabs.f64N/A

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

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

            \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
          4. sqr-powN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
          5. fabs-sqrN/A

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

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

            \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
          8. unpow188.0

            \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
        6. Applied rewrites88.0%

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{3}{2}} \cdot x + \frac{-1}{2} \cdot y \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{3}{2}, x, \frac{-1}{2} \cdot y\right)} \]
          6. lower-*.f6488.2

            \[\leadsto \mathsf{fma}\left(1.5, x, \color{blue}{-0.5 \cdot y}\right) \]
        9. Applied rewrites88.2%

          \[\leadsto \color{blue}{\mathsf{fma}\left(1.5, x, -0.5 \cdot y\right)} \]
      3. Recombined 3 regimes into one program.
      4. Add Preprocessing

      Alternative 5: 84.1% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.3 \cdot 10^{-127}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\ \;\;\;\;\mathsf{fma}\left(\left|-y\right|, 0.5, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\ \end{array} \end{array} \]
      (FPCore (x y)
       :precision binary64
       (if (<= x -2.3e-127)
         (* (+ y x) 0.5)
         (if (<= x 4.6e-35) (fma (fabs (- y)) 0.5 x) (fma (- x y) 0.5 x))))
      double code(double x, double y) {
      	double tmp;
      	if (x <= -2.3e-127) {
      		tmp = (y + x) * 0.5;
      	} else if (x <= 4.6e-35) {
      		tmp = fma(fabs(-y), 0.5, x);
      	} else {
      		tmp = fma((x - y), 0.5, x);
      	}
      	return tmp;
      }
      
      function code(x, y)
      	tmp = 0.0
      	if (x <= -2.3e-127)
      		tmp = Float64(Float64(y + x) * 0.5);
      	elseif (x <= 4.6e-35)
      		tmp = fma(abs(Float64(-y)), 0.5, x);
      	else
      		tmp = fma(Float64(x - y), 0.5, x);
      	end
      	return tmp
      end
      
      code[x_, y_] := If[LessEqual[x, -2.3e-127], N[(N[(y + x), $MachinePrecision] * 0.5), $MachinePrecision], If[LessEqual[x, 4.6e-35], N[(N[Abs[(-y)], $MachinePrecision] * 0.5 + x), $MachinePrecision], N[(N[(x - y), $MachinePrecision] * 0.5 + x), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;x \leq -2.3 \cdot 10^{-127}:\\
      \;\;\;\;\left(y + x\right) \cdot 0.5\\
      
      \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\
      \;\;\;\;\mathsf{fma}\left(\left|-y\right|, 0.5, x\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if x < -2.30000000000000019e-127

        1. Initial program 100.0%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval100.0

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fma.f64N/A

            \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
          2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
          3. unpow2N/A

            \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
          4. rem-square-sqrtN/A

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

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

            \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
          7. lower-*.f6475.7

            \[\leadsto \color{blue}{0.5 \cdot x} \]
        9. Applied rewrites75.7%

          \[\leadsto \color{blue}{0.5 \cdot x} \]
        10. Taylor expanded in x around -inf

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

          \[\leadsto \color{blue}{\left(y + x\right) \cdot 0.5} \]

        if -2.30000000000000019e-127 < x < 4.5999999999999998e-35

        1. Initial program 100.0%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval100.0

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

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

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-1 \cdot y}\right|, \frac{1}{2}, x\right) \]
        6. Step-by-step derivation
          1. mul-1-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\mathsf{neg}\left(y\right)}\right|, \frac{1}{2}, x\right) \]
          2. lower-neg.f6488.4

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-y}\right|, 0.5, x\right) \]
        7. Applied rewrites88.4%

          \[\leadsto \mathsf{fma}\left(\left|\color{blue}{-y}\right|, 0.5, x\right) \]

        if 4.5999999999999998e-35 < x

        1. Initial program 99.8%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval99.8

            \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
        4. Applied rewrites99.8%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fabs.f64N/A

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

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

            \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
          4. sqr-powN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
          5. fabs-sqrN/A

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

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

            \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
          8. unpow188.0

            \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
        6. Applied rewrites88.0%

          \[\leadsto \color{blue}{\mathsf{fma}\left(x - y, 0.5, x\right)} \]
      3. Recombined 3 regimes into one program.
      4. Add Preprocessing

      Alternative 6: 83.6% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.8 \cdot 10^{-129}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\ \;\;\;\;\left|y - x\right| \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\ \end{array} \end{array} \]
      (FPCore (x y)
       :precision binary64
       (if (<= x -2.8e-129)
         (* (+ y x) 0.5)
         (if (<= x 4.6e-35) (* (fabs (- y x)) 0.5) (fma (- x y) 0.5 x))))
      double code(double x, double y) {
      	double tmp;
      	if (x <= -2.8e-129) {
      		tmp = (y + x) * 0.5;
      	} else if (x <= 4.6e-35) {
      		tmp = fabs((y - x)) * 0.5;
      	} else {
      		tmp = fma((x - y), 0.5, x);
      	}
      	return tmp;
      }
      
      function code(x, y)
      	tmp = 0.0
      	if (x <= -2.8e-129)
      		tmp = Float64(Float64(y + x) * 0.5);
      	elseif (x <= 4.6e-35)
      		tmp = Float64(abs(Float64(y - x)) * 0.5);
      	else
      		tmp = fma(Float64(x - y), 0.5, x);
      	end
      	return tmp
      end
      
      code[x_, y_] := If[LessEqual[x, -2.8e-129], N[(N[(y + x), $MachinePrecision] * 0.5), $MachinePrecision], If[LessEqual[x, 4.6e-35], N[(N[Abs[N[(y - x), $MachinePrecision]], $MachinePrecision] * 0.5), $MachinePrecision], N[(N[(x - y), $MachinePrecision] * 0.5 + x), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;x \leq -2.8 \cdot 10^{-129}:\\
      \;\;\;\;\left(y + x\right) \cdot 0.5\\
      
      \mathbf{elif}\;x \leq 4.6 \cdot 10^{-35}:\\
      \;\;\;\;\left|y - x\right| \cdot 0.5\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if x < -2.7999999999999999e-129

        1. Initial program 100.0%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval100.0

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fma.f64N/A

            \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
          2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
          3. unpow2N/A

            \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
          4. rem-square-sqrtN/A

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

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

            \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
          7. lower-*.f6475.7

            \[\leadsto \color{blue}{0.5 \cdot x} \]
        9. Applied rewrites75.7%

          \[\leadsto \color{blue}{0.5 \cdot x} \]
        10. Taylor expanded in x around -inf

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

          \[\leadsto \color{blue}{\left(y + x\right) \cdot 0.5} \]

        if -2.7999999999999999e-129 < x < 4.5999999999999998e-35

        1. Initial program 100.0%

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

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

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

            \[\leadsto \left|\color{blue}{y + \left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
          3. mul-1-negN/A

            \[\leadsto \left|y + \color{blue}{-1 \cdot x}\right| \cdot \frac{1}{2} \]
          4. lower-*.f64N/A

            \[\leadsto \color{blue}{\left|y + -1 \cdot x\right| \cdot \frac{1}{2}} \]
          5. mul-1-negN/A

            \[\leadsto \left|y + \color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
          6. remove-double-negN/A

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

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

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

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

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

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

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

            \[\leadsto \left|\left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(y\right)\right)}\right)\right) + \left(\mathsf{neg}\left(x\right)\right)\right| \cdot \frac{1}{2} \]
          14. remove-double-negN/A

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

            \[\leadsto \left|\color{blue}{y - x}\right| \cdot \frac{1}{2} \]
          16. lower--.f6487.5

            \[\leadsto \left|\color{blue}{y - x}\right| \cdot 0.5 \]
        5. Applied rewrites87.5%

          \[\leadsto \color{blue}{\left|y - x\right| \cdot 0.5} \]

        if 4.5999999999999998e-35 < x

        1. Initial program 99.8%

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

            \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
          2. +-commutativeN/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
          3. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
          4. div-invN/A

            \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
          5. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
          6. lift-fabs.f64N/A

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
          7. neg-fabsN/A

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

            \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
          9. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
          10. sub-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
          11. +-commutativeN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
          13. remove-double-negN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
          14. sub-negN/A

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

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
          16. metadata-eval99.8

            \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
        4. Applied rewrites99.8%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
        5. Step-by-step derivation
          1. lift-fabs.f64N/A

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

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

            \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
          4. sqr-powN/A

            \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
          5. fabs-sqrN/A

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

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

            \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
          8. unpow188.0

            \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
        6. Applied rewrites88.0%

          \[\leadsto \color{blue}{\mathsf{fma}\left(x - y, 0.5, x\right)} \]
      3. Recombined 3 regimes into one program.
      4. Add Preprocessing

      Alternative 7: 78.7% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq -1.2 \cdot 10^{-254}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{elif}\;y \leq 1.7 \cdot 10^{-271}:\\ \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \end{array} \end{array} \]
      (FPCore (x y)
       :precision binary64
       (if (<= y -1.2e-254)
         (* 0.5 (- x y))
         (if (<= y 1.7e-271) (fma (- x y) 0.5 x) (* (+ y x) 0.5))))
      double code(double x, double y) {
      	double tmp;
      	if (y <= -1.2e-254) {
      		tmp = 0.5 * (x - y);
      	} else if (y <= 1.7e-271) {
      		tmp = fma((x - y), 0.5, x);
      	} else {
      		tmp = (y + x) * 0.5;
      	}
      	return tmp;
      }
      
      function code(x, y)
      	tmp = 0.0
      	if (y <= -1.2e-254)
      		tmp = Float64(0.5 * Float64(x - y));
      	elseif (y <= 1.7e-271)
      		tmp = fma(Float64(x - y), 0.5, x);
      	else
      		tmp = Float64(Float64(y + x) * 0.5);
      	end
      	return tmp
      end
      
      code[x_, y_] := If[LessEqual[y, -1.2e-254], N[(0.5 * N[(x - y), $MachinePrecision]), $MachinePrecision], If[LessEqual[y, 1.7e-271], N[(N[(x - y), $MachinePrecision] * 0.5 + x), $MachinePrecision], N[(N[(y + x), $MachinePrecision] * 0.5), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;y \leq -1.2 \cdot 10^{-254}:\\
      \;\;\;\;0.5 \cdot \left(x - y\right)\\
      
      \mathbf{elif}\;y \leq 1.7 \cdot 10^{-271}:\\
      \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\left(y + x\right) \cdot 0.5\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if y < -1.20000000000000001e-254

        1. Initial program 99.9%

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

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

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

            \[\leadsto \left|\color{blue}{y + \left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
          3. mul-1-negN/A

            \[\leadsto \left|y + \color{blue}{-1 \cdot x}\right| \cdot \frac{1}{2} \]
          4. lower-*.f64N/A

            \[\leadsto \color{blue}{\left|y + -1 \cdot x\right| \cdot \frac{1}{2}} \]
          5. mul-1-negN/A

            \[\leadsto \left|y + \color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
          6. remove-double-negN/A

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

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

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

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

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

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

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

            \[\leadsto \left|\left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(y\right)\right)}\right)\right) + \left(\mathsf{neg}\left(x\right)\right)\right| \cdot \frac{1}{2} \]
          14. remove-double-negN/A

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

            \[\leadsto \left|\color{blue}{y - x}\right| \cdot \frac{1}{2} \]
          16. lower--.f6458.3

            \[\leadsto \left|\color{blue}{y - x}\right| \cdot 0.5 \]
        5. Applied rewrites58.3%

          \[\leadsto \color{blue}{\left|y - x\right| \cdot 0.5} \]
        6. Step-by-step derivation
          1. Applied rewrites83.1%

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

          if -1.20000000000000001e-254 < y < 1.7e-271

          1. Initial program 99.9%

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

              \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
            3. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
            4. div-invN/A

              \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
            6. lift-fabs.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
            7. neg-fabsN/A

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

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
            9. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
            10. sub-negN/A

              \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
            11. +-commutativeN/A

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

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
            13. remove-double-negN/A

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
            14. sub-negN/A

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

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
            16. metadata-eval99.9

              \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
          4. Applied rewrites99.9%

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
          5. Step-by-step derivation
            1. lift-fabs.f64N/A

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

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

              \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
            4. sqr-powN/A

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
            5. fabs-sqrN/A

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

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

              \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
            8. unpow172.5

              \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
          6. Applied rewrites72.5%

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

          if 1.7e-271 < y

          1. Initial program 99.9%

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

              \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
            3. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
            4. div-invN/A

              \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
            5. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
            6. lift-fabs.f64N/A

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
            7. neg-fabsN/A

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

              \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
            9. lift--.f64N/A

              \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
            10. sub-negN/A

              \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
            11. +-commutativeN/A

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

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
            13. remove-double-negN/A

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
            14. sub-negN/A

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

              \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
            16. metadata-eval99.9

              \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
          4. Applied rewrites99.9%

            \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
          5. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
            2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

              \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
            3. unpow2N/A

              \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
            4. rem-square-sqrtN/A

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

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

              \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
            7. lower-*.f6434.7

              \[\leadsto \color{blue}{0.5 \cdot x} \]
          9. Applied rewrites34.7%

            \[\leadsto \color{blue}{0.5 \cdot x} \]
          10. Taylor expanded in x around -inf

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

            \[\leadsto \color{blue}{\left(y + x\right) \cdot 0.5} \]
        7. Recombined 3 regimes into one program.
        8. Final simplification81.7%

          \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -1.2 \cdot 10^{-254}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{elif}\;y \leq 1.7 \cdot 10^{-271}:\\ \;\;\;\;\mathsf{fma}\left(x - y, 0.5, x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \end{array} \]
        9. Add Preprocessing

        Alternative 8: 78.6% accurate, 1.0× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq -4.6 \cdot 10^{-257}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{elif}\;y \leq 1.25 \cdot 10^{-295}:\\ \;\;\;\;1.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \end{array} \end{array} \]
        (FPCore (x y)
         :precision binary64
         (if (<= y -4.6e-257)
           (* 0.5 (- x y))
           (if (<= y 1.25e-295) (* 1.5 x) (* (+ y x) 0.5))))
        double code(double x, double y) {
        	double tmp;
        	if (y <= -4.6e-257) {
        		tmp = 0.5 * (x - y);
        	} else if (y <= 1.25e-295) {
        		tmp = 1.5 * x;
        	} else {
        		tmp = (y + x) * 0.5;
        	}
        	return tmp;
        }
        
        real(8) function code(x, y)
            real(8), intent (in) :: x
            real(8), intent (in) :: y
            real(8) :: tmp
            if (y <= (-4.6d-257)) then
                tmp = 0.5d0 * (x - y)
            else if (y <= 1.25d-295) then
                tmp = 1.5d0 * x
            else
                tmp = (y + x) * 0.5d0
            end if
            code = tmp
        end function
        
        public static double code(double x, double y) {
        	double tmp;
        	if (y <= -4.6e-257) {
        		tmp = 0.5 * (x - y);
        	} else if (y <= 1.25e-295) {
        		tmp = 1.5 * x;
        	} else {
        		tmp = (y + x) * 0.5;
        	}
        	return tmp;
        }
        
        def code(x, y):
        	tmp = 0
        	if y <= -4.6e-257:
        		tmp = 0.5 * (x - y)
        	elif y <= 1.25e-295:
        		tmp = 1.5 * x
        	else:
        		tmp = (y + x) * 0.5
        	return tmp
        
        function code(x, y)
        	tmp = 0.0
        	if (y <= -4.6e-257)
        		tmp = Float64(0.5 * Float64(x - y));
        	elseif (y <= 1.25e-295)
        		tmp = Float64(1.5 * x);
        	else
        		tmp = Float64(Float64(y + x) * 0.5);
        	end
        	return tmp
        end
        
        function tmp_2 = code(x, y)
        	tmp = 0.0;
        	if (y <= -4.6e-257)
        		tmp = 0.5 * (x - y);
        	elseif (y <= 1.25e-295)
        		tmp = 1.5 * x;
        	else
        		tmp = (y + x) * 0.5;
        	end
        	tmp_2 = tmp;
        end
        
        code[x_, y_] := If[LessEqual[y, -4.6e-257], N[(0.5 * N[(x - y), $MachinePrecision]), $MachinePrecision], If[LessEqual[y, 1.25e-295], N[(1.5 * x), $MachinePrecision], N[(N[(y + x), $MachinePrecision] * 0.5), $MachinePrecision]]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;y \leq -4.6 \cdot 10^{-257}:\\
        \;\;\;\;0.5 \cdot \left(x - y\right)\\
        
        \mathbf{elif}\;y \leq 1.25 \cdot 10^{-295}:\\
        \;\;\;\;1.5 \cdot x\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(y + x\right) \cdot 0.5\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 3 regimes
        2. if y < -4.6e-257

          1. Initial program 99.9%

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

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

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

              \[\leadsto \left|\color{blue}{y + \left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
            3. mul-1-negN/A

              \[\leadsto \left|y + \color{blue}{-1 \cdot x}\right| \cdot \frac{1}{2} \]
            4. lower-*.f64N/A

              \[\leadsto \color{blue}{\left|y + -1 \cdot x\right| \cdot \frac{1}{2}} \]
            5. mul-1-negN/A

              \[\leadsto \left|y + \color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
            6. remove-double-negN/A

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

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

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

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

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

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

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

              \[\leadsto \left|\left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(y\right)\right)}\right)\right) + \left(\mathsf{neg}\left(x\right)\right)\right| \cdot \frac{1}{2} \]
            14. remove-double-negN/A

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

              \[\leadsto \left|\color{blue}{y - x}\right| \cdot \frac{1}{2} \]
            16. lower--.f6458.3

              \[\leadsto \left|\color{blue}{y - x}\right| \cdot 0.5 \]
          5. Applied rewrites58.3%

            \[\leadsto \color{blue}{\left|y - x\right| \cdot 0.5} \]
          6. Step-by-step derivation
            1. Applied rewrites83.1%

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

            if -4.6e-257 < y < 1.25000000000000002e-295

            1. Initial program 99.9%

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

                \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
              4. div-invN/A

                \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
              5. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
              6. lift-fabs.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
              7. neg-fabsN/A

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
              9. lift--.f64N/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
              10. sub-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
              11. +-commutativeN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
              13. remove-double-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
              14. sub-negN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
              16. metadata-eval99.9

                \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
            5. Step-by-step derivation
              1. lift-fabs.f64N/A

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

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

                \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
              4. sqr-powN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
              5. fabs-sqrN/A

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

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

                \[\leadsto \mathsf{fma}\left({\left(x - y\right)}^{\color{blue}{1}}, \frac{1}{2}, x\right) \]
              8. unpow180.9

                \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
            6. Applied rewrites80.9%

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

              \[\leadsto \color{blue}{x + \frac{1}{2} \cdot x} \]
            8. Step-by-step derivation
              1. distribute-rgt1-inN/A

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

                \[\leadsto \color{blue}{\frac{3}{2}} \cdot x \]
              3. lower-*.f6473.8

                \[\leadsto \color{blue}{1.5 \cdot x} \]
            9. Applied rewrites73.8%

              \[\leadsto \color{blue}{1.5 \cdot x} \]

            if 1.25000000000000002e-295 < y

            1. Initial program 99.9%

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

                \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
              4. div-invN/A

                \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
              5. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
              6. lift-fabs.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
              7. neg-fabsN/A

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
              9. lift--.f64N/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
              10. sub-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
              11. +-commutativeN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
              13. remove-double-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
              14. sub-negN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
              16. metadata-eval99.9

                \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
            5. Step-by-step derivation
              1. lift-fma.f64N/A

                \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
              2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

                \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
              3. unpow2N/A

                \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
              4. rem-square-sqrtN/A

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

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

                \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
              7. lower-*.f6436.2

                \[\leadsto \color{blue}{0.5 \cdot x} \]
            9. Applied rewrites36.2%

              \[\leadsto \color{blue}{0.5 \cdot x} \]
            10. Taylor expanded in x around -inf

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

              \[\leadsto \color{blue}{\left(y + x\right) \cdot 0.5} \]
          7. Recombined 3 regimes into one program.
          8. Final simplification81.3%

            \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -4.6 \cdot 10^{-257}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{elif}\;y \leq 1.25 \cdot 10^{-295}:\\ \;\;\;\;1.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(y + x\right) \cdot 0.5\\ \end{array} \]
          9. Add Preprocessing

          Alternative 9: 59.8% accurate, 1.1× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq -7.2 \cdot 10^{-72}:\\ \;\;\;\;-0.5 \cdot y\\ \mathbf{elif}\;y \leq 2.45 \cdot 10^{+27}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \end{array} \]
          (FPCore (x y)
           :precision binary64
           (if (<= y -7.2e-72) (* -0.5 y) (if (<= y 2.45e+27) (* 0.5 x) (* 0.5 y))))
          double code(double x, double y) {
          	double tmp;
          	if (y <= -7.2e-72) {
          		tmp = -0.5 * y;
          	} else if (y <= 2.45e+27) {
          		tmp = 0.5 * x;
          	} else {
          		tmp = 0.5 * y;
          	}
          	return tmp;
          }
          
          real(8) function code(x, y)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              real(8) :: tmp
              if (y <= (-7.2d-72)) then
                  tmp = (-0.5d0) * y
              else if (y <= 2.45d+27) then
                  tmp = 0.5d0 * x
              else
                  tmp = 0.5d0 * y
              end if
              code = tmp
          end function
          
          public static double code(double x, double y) {
          	double tmp;
          	if (y <= -7.2e-72) {
          		tmp = -0.5 * y;
          	} else if (y <= 2.45e+27) {
          		tmp = 0.5 * x;
          	} else {
          		tmp = 0.5 * y;
          	}
          	return tmp;
          }
          
          def code(x, y):
          	tmp = 0
          	if y <= -7.2e-72:
          		tmp = -0.5 * y
          	elif y <= 2.45e+27:
          		tmp = 0.5 * x
          	else:
          		tmp = 0.5 * y
          	return tmp
          
          function code(x, y)
          	tmp = 0.0
          	if (y <= -7.2e-72)
          		tmp = Float64(-0.5 * y);
          	elseif (y <= 2.45e+27)
          		tmp = Float64(0.5 * x);
          	else
          		tmp = Float64(0.5 * y);
          	end
          	return tmp
          end
          
          function tmp_2 = code(x, y)
          	tmp = 0.0;
          	if (y <= -7.2e-72)
          		tmp = -0.5 * y;
          	elseif (y <= 2.45e+27)
          		tmp = 0.5 * x;
          	else
          		tmp = 0.5 * y;
          	end
          	tmp_2 = tmp;
          end
          
          code[x_, y_] := If[LessEqual[y, -7.2e-72], N[(-0.5 * y), $MachinePrecision], If[LessEqual[y, 2.45e+27], N[(0.5 * x), $MachinePrecision], N[(0.5 * y), $MachinePrecision]]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;y \leq -7.2 \cdot 10^{-72}:\\
          \;\;\;\;-0.5 \cdot y\\
          
          \mathbf{elif}\;y \leq 2.45 \cdot 10^{+27}:\\
          \;\;\;\;0.5 \cdot x\\
          
          \mathbf{else}:\\
          \;\;\;\;0.5 \cdot y\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 3 regimes
          2. if y < -7.2e-72

            1. Initial program 99.9%

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

                \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
              4. div-invN/A

                \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
              5. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
              6. lift-fabs.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
              7. neg-fabsN/A

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
              9. lift--.f64N/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
              10. sub-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
              11. +-commutativeN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
              13. remove-double-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
              14. sub-negN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
              16. metadata-eval99.9

                \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
            5. Step-by-step derivation
              1. lift-fabs.f64N/A

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

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

                \[\leadsto \mathsf{fma}\left(\left|{\left(x - y\right)}^{\color{blue}{\left(\frac{1}{2} \cdot 2\right)}}\right|, \frac{1}{2}, x\right) \]
              4. sqr-powN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{{\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)} \cdot {\left(x - y\right)}^{\left(\frac{\frac{1}{2} \cdot 2}{2}\right)}}\right|, \frac{1}{2}, x\right) \]
              5. fabs-sqrN/A

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

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

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{x - y}, 0.5, x\right) \]
            6. Applied rewrites85.2%

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

              \[\leadsto \color{blue}{\frac{-1}{2} \cdot y} \]
            8. Step-by-step derivation
              1. lower-*.f6468.6

                \[\leadsto \color{blue}{-0.5 \cdot y} \]
            9. Applied rewrites68.6%

              \[\leadsto \color{blue}{-0.5 \cdot y} \]

            if -7.2e-72 < y < 2.45000000000000007e27

            1. Initial program 99.9%

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

                \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
              4. div-invN/A

                \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
              5. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
              6. lift-fabs.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
              7. neg-fabsN/A

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
              9. lift--.f64N/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
              10. sub-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
              11. +-commutativeN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
              13. remove-double-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
              14. sub-negN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
              16. metadata-eval99.9

                \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
            4. Applied rewrites99.9%

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
            5. Step-by-step derivation
              1. lift-fma.f64N/A

                \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
              2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

                \[\leadsto \color{blue}{\left(-1 \cdot \left({\left(\sqrt{\frac{1}{2}}\right)}^{2} - 1\right)\right) \cdot x} \]
              3. unpow2N/A

                \[\leadsto \left(-1 \cdot \left(\color{blue}{\sqrt{\frac{1}{2}} \cdot \sqrt{\frac{1}{2}}} - 1\right)\right) \cdot x \]
              4. rem-square-sqrtN/A

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

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

                \[\leadsto \color{blue}{\frac{1}{2}} \cdot x \]
              7. lower-*.f6446.6

                \[\leadsto \color{blue}{0.5 \cdot x} \]
            9. Applied rewrites46.6%

              \[\leadsto \color{blue}{0.5 \cdot x} \]

            if 2.45000000000000007e27 < y

            1. Initial program 100.0%

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

                \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
              4. div-invN/A

                \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
              5. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
              6. lift-fabs.f64N/A

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
              7. neg-fabsN/A

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

                \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
              9. lift--.f64N/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
              10. sub-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
              11. +-commutativeN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
              13. remove-double-negN/A

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
              14. sub-negN/A

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

                \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
              16. metadata-eval100.0

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

              \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
            5. Step-by-step derivation
              1. lift-fma.f64N/A

                \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
              2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

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

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

                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(-1 \cdot \frac{y \cdot {\left(\sqrt{\frac{1}{2}}\right)}^{2}}{x} + {\left(\sqrt{\frac{1}{2}}\right)}^{2}\right) - 1\right)\right)\right) \cdot x} \]
            9. Applied rewrites70.1%

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

              \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]
            11. Step-by-step derivation
              1. Applied rewrites68.2%

                \[\leadsto y \cdot \color{blue}{0.5} \]
            12. Recombined 3 regimes into one program.
            13. Final simplification58.1%

              \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -7.2 \cdot 10^{-72}:\\ \;\;\;\;-0.5 \cdot y\\ \mathbf{elif}\;y \leq 2.45 \cdot 10^{+27}:\\ \;\;\;\;0.5 \cdot x\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]
            14. Add Preprocessing

            Alternative 10: 67.8% accurate, 1.3× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq 2.45 \cdot 10^{+27}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \end{array} \]
            (FPCore (x y)
             :precision binary64
             (if (<= y 2.45e+27) (* 0.5 (- x y)) (* 0.5 y)))
            double code(double x, double y) {
            	double tmp;
            	if (y <= 2.45e+27) {
            		tmp = 0.5 * (x - y);
            	} else {
            		tmp = 0.5 * y;
            	}
            	return tmp;
            }
            
            real(8) function code(x, y)
                real(8), intent (in) :: x
                real(8), intent (in) :: y
                real(8) :: tmp
                if (y <= 2.45d+27) then
                    tmp = 0.5d0 * (x - y)
                else
                    tmp = 0.5d0 * y
                end if
                code = tmp
            end function
            
            public static double code(double x, double y) {
            	double tmp;
            	if (y <= 2.45e+27) {
            		tmp = 0.5 * (x - y);
            	} else {
            		tmp = 0.5 * y;
            	}
            	return tmp;
            }
            
            def code(x, y):
            	tmp = 0
            	if y <= 2.45e+27:
            		tmp = 0.5 * (x - y)
            	else:
            		tmp = 0.5 * y
            	return tmp
            
            function code(x, y)
            	tmp = 0.0
            	if (y <= 2.45e+27)
            		tmp = Float64(0.5 * Float64(x - y));
            	else
            		tmp = Float64(0.5 * y);
            	end
            	return tmp
            end
            
            function tmp_2 = code(x, y)
            	tmp = 0.0;
            	if (y <= 2.45e+27)
            		tmp = 0.5 * (x - y);
            	else
            		tmp = 0.5 * y;
            	end
            	tmp_2 = tmp;
            end
            
            code[x_, y_] := If[LessEqual[y, 2.45e+27], N[(0.5 * N[(x - y), $MachinePrecision]), $MachinePrecision], N[(0.5 * y), $MachinePrecision]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;y \leq 2.45 \cdot 10^{+27}:\\
            \;\;\;\;0.5 \cdot \left(x - y\right)\\
            
            \mathbf{else}:\\
            \;\;\;\;0.5 \cdot y\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if y < 2.45000000000000007e27

              1. Initial program 99.9%

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

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

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

                  \[\leadsto \left|\color{blue}{y + \left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
                3. mul-1-negN/A

                  \[\leadsto \left|y + \color{blue}{-1 \cdot x}\right| \cdot \frac{1}{2} \]
                4. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left|y + -1 \cdot x\right| \cdot \frac{1}{2}} \]
                5. mul-1-negN/A

                  \[\leadsto \left|y + \color{blue}{\left(\mathsf{neg}\left(x\right)\right)}\right| \cdot \frac{1}{2} \]
                6. remove-double-negN/A

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

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

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

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

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

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

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

                  \[\leadsto \left|\left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(y\right)\right)}\right)\right) + \left(\mathsf{neg}\left(x\right)\right)\right| \cdot \frac{1}{2} \]
                14. remove-double-negN/A

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

                  \[\leadsto \left|\color{blue}{y - x}\right| \cdot \frac{1}{2} \]
                16. lower--.f6446.0

                  \[\leadsto \left|\color{blue}{y - x}\right| \cdot 0.5 \]
              5. Applied rewrites46.0%

                \[\leadsto \color{blue}{\left|y - x\right| \cdot 0.5} \]
              6. Step-by-step derivation
                1. Applied rewrites67.6%

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

                if 2.45000000000000007e27 < y

                1. Initial program 100.0%

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

                    \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
                  2. +-commutativeN/A

                    \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
                  3. lift-/.f64N/A

                    \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
                  4. div-invN/A

                    \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
                  5. lower-fma.f64N/A

                    \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
                  6. lift-fabs.f64N/A

                    \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
                  7. neg-fabsN/A

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

                    \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
                  9. lift--.f64N/A

                    \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
                  10. sub-negN/A

                    \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
                  11. +-commutativeN/A

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

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
                  13. remove-double-negN/A

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
                  14. sub-negN/A

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

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
                  16. metadata-eval100.0

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

                  \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
                5. Step-by-step derivation
                  1. lift-fma.f64N/A

                    \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
                  2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

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

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

                    \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(-1 \cdot \frac{y \cdot {\left(\sqrt{\frac{1}{2}}\right)}^{2}}{x} + {\left(\sqrt{\frac{1}{2}}\right)}^{2}\right) - 1\right)\right)\right) \cdot x} \]
                9. Applied rewrites70.1%

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

                  \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]
                11. Step-by-step derivation
                  1. Applied rewrites68.2%

                    \[\leadsto y \cdot \color{blue}{0.5} \]
                12. Recombined 2 regimes into one program.
                13. Final simplification67.7%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq 2.45 \cdot 10^{+27}:\\ \;\;\;\;0.5 \cdot \left(x - y\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]
                14. Add Preprocessing

                Alternative 11: 27.1% accurate, 3.3× speedup?

                \[\begin{array}{l} \\ 0.5 \cdot y \end{array} \]
                (FPCore (x y) :precision binary64 (* 0.5 y))
                double code(double x, double y) {
                	return 0.5 * y;
                }
                
                real(8) function code(x, y)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    code = 0.5d0 * y
                end function
                
                public static double code(double x, double y) {
                	return 0.5 * y;
                }
                
                def code(x, y):
                	return 0.5 * y
                
                function code(x, y)
                	return Float64(0.5 * y)
                end
                
                function tmp = code(x, y)
                	tmp = 0.5 * y;
                end
                
                code[x_, y_] := N[(0.5 * y), $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                0.5 \cdot y
                \end{array}
                
                Derivation
                1. Initial program 99.9%

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

                    \[\leadsto \color{blue}{x + \frac{\left|y - x\right|}{2}} \]
                  2. +-commutativeN/A

                    \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2} + x} \]
                  3. lift-/.f64N/A

                    \[\leadsto \color{blue}{\frac{\left|y - x\right|}{2}} + x \]
                  4. div-invN/A

                    \[\leadsto \color{blue}{\left|y - x\right| \cdot \frac{1}{2}} + x \]
                  5. lower-fma.f64N/A

                    \[\leadsto \color{blue}{\mathsf{fma}\left(\left|y - x\right|, \frac{1}{2}, x\right)} \]
                  6. lift-fabs.f64N/A

                    \[\leadsto \mathsf{fma}\left(\color{blue}{\left|y - x\right|}, \frac{1}{2}, x\right) \]
                  7. neg-fabsN/A

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

                    \[\leadsto \mathsf{fma}\left(\color{blue}{\left|\mathsf{neg}\left(\left(y - x\right)\right)\right|}, \frac{1}{2}, x\right) \]
                  9. lift--.f64N/A

                    \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y - x\right)}\right)\right|, \frac{1}{2}, x\right) \]
                  10. sub-negN/A

                    \[\leadsto \mathsf{fma}\left(\left|\mathsf{neg}\left(\color{blue}{\left(y + \left(\mathsf{neg}\left(x\right)\right)\right)}\right)\right|, \frac{1}{2}, x\right) \]
                  11. +-commutativeN/A

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

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(x\right)\right)\right)\right) + \left(\mathsf{neg}\left(y\right)\right)}\right|, \frac{1}{2}, x\right) \]
                  13. remove-double-negN/A

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x} + \left(\mathsf{neg}\left(y\right)\right)\right|, \frac{1}{2}, x\right) \]
                  14. sub-negN/A

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

                    \[\leadsto \mathsf{fma}\left(\left|\color{blue}{x - y}\right|, \frac{1}{2}, x\right) \]
                  16. metadata-eval99.9

                    \[\leadsto \mathsf{fma}\left(\left|x - y\right|, \color{blue}{0.5}, x\right) \]
                4. Applied rewrites99.9%

                  \[\leadsto \color{blue}{\mathsf{fma}\left(\left|x - y\right|, 0.5, x\right)} \]
                5. Step-by-step derivation
                  1. lift-fma.f64N/A

                    \[\leadsto \color{blue}{\left|x - y\right| \cdot \frac{1}{2} + x} \]
                  2. unpow1N/A

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

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

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

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

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

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

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

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

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

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

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

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

                    \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(-1 \cdot \frac{y \cdot {\left(\sqrt{\frac{1}{2}}\right)}^{2}}{x} + {\left(\sqrt{\frac{1}{2}}\right)}^{2}\right) - 1\right)\right)\right) \cdot x} \]
                9. Applied rewrites50.8%

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

                  \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]
                11. Step-by-step derivation
                  1. Applied rewrites23.5%

                    \[\leadsto y \cdot \color{blue}{0.5} \]
                  2. Final simplification23.5%

                    \[\leadsto 0.5 \cdot y \]
                  3. Add Preprocessing

                  Reproduce

                  ?
                  herbie shell --seed 2024270 
                  (FPCore (x y)
                    :name "Graphics.Rendering.Chart.Plot.AreaSpots:renderSpotLegend from Chart-1.5.3"
                    :precision binary64
                    (+ x (/ (fabs (- y x)) 2.0)))