Numeric.SpecFunctions:logGamma from math-functions-0.1.5.2, A

Percentage Accurate: 100.0% → 100.0%
Time: 7.6s
Alternatives: 12
Speedup: 1.2×

Specification

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

\\
\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673
\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 12 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: 100.0% accurate, 1.0× speedup?

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

\\
\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673
\end{array}

Alternative 1: 100.0% accurate, 1.0× speedup?

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

\\
0.918938533204673 - \left(y \cdot 0.5 - x \cdot \left(y + -1\right)\right)
\end{array}
Derivation
  1. Initial program 100.0%

    \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
  2. Add Preprocessing
  3. Final simplification100.0%

    \[\leadsto 0.918938533204673 - \left(y \cdot 0.5 - x \cdot \left(y + -1\right)\right) \]
  4. Add Preprocessing

Alternative 2: 73.9% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := x \cdot \left(y + -1\right)\\ \mathbf{if}\;x \leq -48000:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;x \leq -9 \cdot 10^{-67}:\\ \;\;\;\;0.918938533204673 - x\\ \mathbf{elif}\;x \leq 1.25 \cdot 10^{-188}:\\ \;\;\;\;y \cdot -0.5\\ \mathbf{elif}\;x \leq 18500000000:\\ \;\;\;\;0.918938533204673 - x\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (let* ((t_0 (* x (+ y -1.0))))
   (if (<= x -48000.0)
     t_0
     (if (<= x -9e-67)
       (- 0.918938533204673 x)
       (if (<= x 1.25e-188)
         (* y -0.5)
         (if (<= x 18500000000.0) (- 0.918938533204673 x) t_0))))))
double code(double x, double y) {
	double t_0 = x * (y + -1.0);
	double tmp;
	if (x <= -48000.0) {
		tmp = t_0;
	} else if (x <= -9e-67) {
		tmp = 0.918938533204673 - x;
	} else if (x <= 1.25e-188) {
		tmp = y * -0.5;
	} else if (x <= 18500000000.0) {
		tmp = 0.918938533204673 - x;
	} else {
		tmp = t_0;
	}
	return tmp;
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8) :: t_0
    real(8) :: tmp
    t_0 = x * (y + (-1.0d0))
    if (x <= (-48000.0d0)) then
        tmp = t_0
    else if (x <= (-9d-67)) then
        tmp = 0.918938533204673d0 - x
    else if (x <= 1.25d-188) then
        tmp = y * (-0.5d0)
    else if (x <= 18500000000.0d0) then
        tmp = 0.918938533204673d0 - x
    else
        tmp = t_0
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double t_0 = x * (y + -1.0);
	double tmp;
	if (x <= -48000.0) {
		tmp = t_0;
	} else if (x <= -9e-67) {
		tmp = 0.918938533204673 - x;
	} else if (x <= 1.25e-188) {
		tmp = y * -0.5;
	} else if (x <= 18500000000.0) {
		tmp = 0.918938533204673 - x;
	} else {
		tmp = t_0;
	}
	return tmp;
}
def code(x, y):
	t_0 = x * (y + -1.0)
	tmp = 0
	if x <= -48000.0:
		tmp = t_0
	elif x <= -9e-67:
		tmp = 0.918938533204673 - x
	elif x <= 1.25e-188:
		tmp = y * -0.5
	elif x <= 18500000000.0:
		tmp = 0.918938533204673 - x
	else:
		tmp = t_0
	return tmp
function code(x, y)
	t_0 = Float64(x * Float64(y + -1.0))
	tmp = 0.0
	if (x <= -48000.0)
		tmp = t_0;
	elseif (x <= -9e-67)
		tmp = Float64(0.918938533204673 - x);
	elseif (x <= 1.25e-188)
		tmp = Float64(y * -0.5);
	elseif (x <= 18500000000.0)
		tmp = Float64(0.918938533204673 - x);
	else
		tmp = t_0;
	end
	return tmp
end
function tmp_2 = code(x, y)
	t_0 = x * (y + -1.0);
	tmp = 0.0;
	if (x <= -48000.0)
		tmp = t_0;
	elseif (x <= -9e-67)
		tmp = 0.918938533204673 - x;
	elseif (x <= 1.25e-188)
		tmp = y * -0.5;
	elseif (x <= 18500000000.0)
		tmp = 0.918938533204673 - x;
	else
		tmp = t_0;
	end
	tmp_2 = tmp;
end
code[x_, y_] := Block[{t$95$0 = N[(x * N[(y + -1.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[x, -48000.0], t$95$0, If[LessEqual[x, -9e-67], N[(0.918938533204673 - x), $MachinePrecision], If[LessEqual[x, 1.25e-188], N[(y * -0.5), $MachinePrecision], If[LessEqual[x, 18500000000.0], N[(0.918938533204673 - x), $MachinePrecision], t$95$0]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := x \cdot \left(y + -1\right)\\
\mathbf{if}\;x \leq -48000:\\
\;\;\;\;t\_0\\

\mathbf{elif}\;x \leq -9 \cdot 10^{-67}:\\
\;\;\;\;0.918938533204673 - x\\

\mathbf{elif}\;x \leq 1.25 \cdot 10^{-188}:\\
\;\;\;\;y \cdot -0.5\\

\mathbf{elif}\;x \leq 18500000000:\\
\;\;\;\;0.918938533204673 - x\\

\mathbf{else}:\\
\;\;\;\;t\_0\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if x < -48000 or 1.85e10 < x

    1. Initial program 100.0%

      \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
    2. Step-by-step derivation
      1. sub-negN/A

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

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
      3. sub-negN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      4. distribute-lft-inN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      5. associate-+r+N/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      6. *-commutativeN/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      7. associate-+l+N/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
      8. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
      9. distribute-rgt-neg-inN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      10. distribute-lft-outN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      11. *-lowering-*.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      12. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      13. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      14. metadata-evalN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      15. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
      17. cancel-sign-sub-invN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
      18. *-lft-identityN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
      19. --lowering--.f6499.9%

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
    3. Simplified99.9%

      \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
    4. Add Preprocessing
    5. Taylor expanded in x around inf

      \[\leadsto \color{blue}{x \cdot \left(y - 1\right)} \]
    6. Step-by-step derivation
      1. *-lowering-*.f64N/A

        \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{\left(y - 1\right)}\right) \]
      2. sub-negN/A

        \[\leadsto \mathsf{*.f64}\left(x, \left(y + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
      3. metadata-evalN/A

        \[\leadsto \mathsf{*.f64}\left(x, \left(y + -1\right)\right) \]
      4. +-lowering-+.f6498.8%

        \[\leadsto \mathsf{*.f64}\left(x, \mathsf{+.f64}\left(y, \color{blue}{-1}\right)\right) \]
    7. Simplified98.8%

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

    if -48000 < x < -9.00000000000000031e-67 or 1.25e-188 < x < 1.85e10

    1. Initial program 100.0%

      \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
    2. Step-by-step derivation
      1. sub-negN/A

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

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
      3. sub-negN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      4. distribute-lft-inN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      5. associate-+r+N/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      6. *-commutativeN/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      7. associate-+l+N/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
      8. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
      9. distribute-rgt-neg-inN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      10. distribute-lft-outN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      11. *-lowering-*.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      12. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      13. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      14. metadata-evalN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      15. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
      17. cancel-sign-sub-invN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
      18. *-lft-identityN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
      19. --lowering--.f6499.9%

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
    3. Simplified99.9%

      \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
    4. Add Preprocessing
    5. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
    6. Step-by-step derivation
      1. --lowering--.f6466.3%

        \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
    7. Simplified66.3%

      \[\leadsto \color{blue}{0.918938533204673 - x} \]

    if -9.00000000000000031e-67 < x < 1.25e-188

    1. Initial program 100.0%

      \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
    2. Step-by-step derivation
      1. sub-negN/A

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

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
      3. sub-negN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      4. distribute-lft-inN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      5. associate-+r+N/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      6. *-commutativeN/A

        \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
      7. associate-+l+N/A

        \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
      8. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
      9. distribute-rgt-neg-inN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      10. distribute-lft-outN/A

        \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      11. *-lowering-*.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      12. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      13. +-lowering-+.f64N/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
      14. metadata-evalN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
      15. +-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
      16. *-commutativeN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
      17. cancel-sign-sub-invN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
      18. *-lft-identityN/A

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
      19. --lowering--.f64100.0%

        \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
    4. Add Preprocessing
    5. Taylor expanded in y around inf

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

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

        \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
      3. metadata-evalN/A

        \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
      4. +-lowering-+.f6467.6%

        \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
    7. Simplified67.6%

      \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
    8. Taylor expanded in x around 0

      \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{\frac{-1}{2}}\right) \]
    9. Step-by-step derivation
      1. Simplified67.6%

        \[\leadsto y \cdot \color{blue}{-0.5} \]
    10. Recombined 3 regimes into one program.
    11. Add Preprocessing

    Alternative 3: 98.0% accurate, 0.5× speedup?

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

      1. Initial program 100.0%

        \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
      2. Step-by-step derivation
        1. sub-negN/A

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

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
        3. sub-negN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        4. distribute-lft-inN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        5. associate-+r+N/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        6. *-commutativeN/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        7. associate-+l+N/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
        8. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
        9. distribute-rgt-neg-inN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        10. distribute-lft-outN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        11. *-lowering-*.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        12. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        13. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        14. metadata-evalN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        15. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
        16. *-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
        17. cancel-sign-sub-invN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
        18. *-lft-identityN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
        19. --lowering--.f64100.0%

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
      3. Simplified100.0%

        \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
      4. Add Preprocessing
      5. Taylor expanded in y around inf

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

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

          \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
        3. metadata-evalN/A

          \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
        4. +-lowering-+.f6498.9%

          \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
      7. Simplified98.9%

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

      if -1.8e5 < y < -5.6e-11

      1. Initial program 100.0%

        \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
      2. Step-by-step derivation
        1. sub-negN/A

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

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
        3. sub-negN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        4. distribute-lft-inN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        5. associate-+r+N/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        6. *-commutativeN/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        7. associate-+l+N/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
        8. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
        9. distribute-rgt-neg-inN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        10. distribute-lft-outN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        11. *-lowering-*.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        12. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        13. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        14. metadata-evalN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        15. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
        16. *-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
        17. cancel-sign-sub-invN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
        18. *-lft-identityN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
        19. --lowering--.f6499.8%

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
      3. Simplified99.8%

        \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
      4. Add Preprocessing
      5. Taylor expanded in x around inf

        \[\leadsto \color{blue}{x \cdot \left(y - 1\right)} \]
      6. Step-by-step derivation
        1. *-lowering-*.f64N/A

          \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{\left(y - 1\right)}\right) \]
        2. sub-negN/A

          \[\leadsto \mathsf{*.f64}\left(x, \left(y + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
        3. metadata-evalN/A

          \[\leadsto \mathsf{*.f64}\left(x, \left(y + -1\right)\right) \]
        4. +-lowering-+.f64100.0%

          \[\leadsto \mathsf{*.f64}\left(x, \mathsf{+.f64}\left(y, \color{blue}{-1}\right)\right) \]
      7. Simplified100.0%

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

      if -5.6e-11 < y < 1.3999999999999999

      1. Initial program 100.0%

        \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
      2. Step-by-step derivation
        1. sub-negN/A

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

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
        3. sub-negN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        4. distribute-lft-inN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        5. associate-+r+N/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        6. *-commutativeN/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        7. associate-+l+N/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
        8. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
        9. distribute-rgt-neg-inN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        10. distribute-lft-outN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        11. *-lowering-*.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        12. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        13. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        14. metadata-evalN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        15. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
        16. *-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
        17. cancel-sign-sub-invN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
        18. *-lft-identityN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
        19. --lowering--.f6499.9%

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
      3. Simplified99.9%

        \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
      4. Add Preprocessing
      5. Taylor expanded in y around 0

        \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
      6. Step-by-step derivation
        1. --lowering--.f6497.0%

          \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
      7. Simplified97.0%

        \[\leadsto \color{blue}{0.918938533204673 - x} \]
    3. Recombined 3 regimes into one program.
    4. Add Preprocessing

    Alternative 4: 73.3% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq -145000:\\ \;\;\;\;y \cdot -0.5\\ \mathbf{elif}\;y \leq 1.55:\\ \;\;\;\;0.918938533204673 - x\\ \mathbf{elif}\;y \leq 3.8 \cdot 10^{+208}:\\ \;\;\;\;x \cdot y\\ \mathbf{else}:\\ \;\;\;\;y \cdot -0.5\\ \end{array} \end{array} \]
    (FPCore (x y)
     :precision binary64
     (if (<= y -145000.0)
       (* y -0.5)
       (if (<= y 1.55)
         (- 0.918938533204673 x)
         (if (<= y 3.8e+208) (* x y) (* y -0.5)))))
    double code(double x, double y) {
    	double tmp;
    	if (y <= -145000.0) {
    		tmp = y * -0.5;
    	} else if (y <= 1.55) {
    		tmp = 0.918938533204673 - x;
    	} else if (y <= 3.8e+208) {
    		tmp = x * y;
    	} else {
    		tmp = y * -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 <= (-145000.0d0)) then
            tmp = y * (-0.5d0)
        else if (y <= 1.55d0) then
            tmp = 0.918938533204673d0 - x
        else if (y <= 3.8d+208) then
            tmp = x * y
        else
            tmp = y * (-0.5d0)
        end if
        code = tmp
    end function
    
    public static double code(double x, double y) {
    	double tmp;
    	if (y <= -145000.0) {
    		tmp = y * -0.5;
    	} else if (y <= 1.55) {
    		tmp = 0.918938533204673 - x;
    	} else if (y <= 3.8e+208) {
    		tmp = x * y;
    	} else {
    		tmp = y * -0.5;
    	}
    	return tmp;
    }
    
    def code(x, y):
    	tmp = 0
    	if y <= -145000.0:
    		tmp = y * -0.5
    	elif y <= 1.55:
    		tmp = 0.918938533204673 - x
    	elif y <= 3.8e+208:
    		tmp = x * y
    	else:
    		tmp = y * -0.5
    	return tmp
    
    function code(x, y)
    	tmp = 0.0
    	if (y <= -145000.0)
    		tmp = Float64(y * -0.5);
    	elseif (y <= 1.55)
    		tmp = Float64(0.918938533204673 - x);
    	elseif (y <= 3.8e+208)
    		tmp = Float64(x * y);
    	else
    		tmp = Float64(y * -0.5);
    	end
    	return tmp
    end
    
    function tmp_2 = code(x, y)
    	tmp = 0.0;
    	if (y <= -145000.0)
    		tmp = y * -0.5;
    	elseif (y <= 1.55)
    		tmp = 0.918938533204673 - x;
    	elseif (y <= 3.8e+208)
    		tmp = x * y;
    	else
    		tmp = y * -0.5;
    	end
    	tmp_2 = tmp;
    end
    
    code[x_, y_] := If[LessEqual[y, -145000.0], N[(y * -0.5), $MachinePrecision], If[LessEqual[y, 1.55], N[(0.918938533204673 - x), $MachinePrecision], If[LessEqual[y, 3.8e+208], N[(x * y), $MachinePrecision], N[(y * -0.5), $MachinePrecision]]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;y \leq -145000:\\
    \;\;\;\;y \cdot -0.5\\
    
    \mathbf{elif}\;y \leq 1.55:\\
    \;\;\;\;0.918938533204673 - x\\
    
    \mathbf{elif}\;y \leq 3.8 \cdot 10^{+208}:\\
    \;\;\;\;x \cdot y\\
    
    \mathbf{else}:\\
    \;\;\;\;y \cdot -0.5\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if y < -145000 or 3.8000000000000002e208 < y

      1. Initial program 100.0%

        \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
      2. Step-by-step derivation
        1. sub-negN/A

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

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
        3. sub-negN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        4. distribute-lft-inN/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        5. associate-+r+N/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        6. *-commutativeN/A

          \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
        7. associate-+l+N/A

          \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
        8. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
        9. distribute-rgt-neg-inN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        10. distribute-lft-outN/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        11. *-lowering-*.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        12. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        13. +-lowering-+.f64N/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
        14. metadata-evalN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
        15. +-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
        16. *-commutativeN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
        17. cancel-sign-sub-invN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
        18. *-lft-identityN/A

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
        19. --lowering--.f64100.0%

          \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
      3. Simplified100.0%

        \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
      4. Add Preprocessing
      5. Taylor expanded in y around inf

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

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

          \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
        3. metadata-evalN/A

          \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
        4. +-lowering-+.f6499.5%

          \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
      7. Simplified99.5%

        \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
      8. Taylor expanded in x around 0

        \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{\frac{-1}{2}}\right) \]
      9. Step-by-step derivation
        1. Simplified61.1%

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

        if -145000 < y < 1.55000000000000004

        1. Initial program 100.0%

          \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
        2. Step-by-step derivation
          1. sub-negN/A

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

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
          3. sub-negN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          4. distribute-lft-inN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          5. associate-+r+N/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          7. associate-+l+N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
          8. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          10. distribute-lft-outN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          11. *-lowering-*.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          13. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          14. metadata-evalN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          15. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
          17. cancel-sign-sub-invN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
          18. *-lft-identityN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
          19. --lowering--.f6499.9%

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
        3. Simplified99.9%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
        4. Add Preprocessing
        5. Taylor expanded in y around 0

          \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
        6. Step-by-step derivation
          1. --lowering--.f6492.4%

            \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
        7. Simplified92.4%

          \[\leadsto \color{blue}{0.918938533204673 - x} \]

        if 1.55000000000000004 < y < 3.8000000000000002e208

        1. Initial program 100.0%

          \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
        2. Step-by-step derivation
          1. sub-negN/A

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

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
          3. sub-negN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          4. distribute-lft-inN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          5. associate-+r+N/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          7. associate-+l+N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
          8. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          10. distribute-lft-outN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          11. *-lowering-*.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          13. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          14. metadata-evalN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          15. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
          17. cancel-sign-sub-invN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
          18. *-lft-identityN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
          19. --lowering--.f64100.0%

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
        3. Simplified100.0%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
        4. Add Preprocessing
        5. Taylor expanded in y around inf

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

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

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
          3. metadata-evalN/A

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
          4. +-lowering-+.f6497.7%

            \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
        7. Simplified97.7%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
        8. Taylor expanded in x around inf

          \[\leadsto \color{blue}{x \cdot y} \]
        9. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto y \cdot \color{blue}{x} \]
          2. *-lowering-*.f6454.1%

            \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{x}\right) \]
        10. Simplified54.1%

          \[\leadsto \color{blue}{y \cdot x} \]
      10. Recombined 3 regimes into one program.
      11. Final simplification74.7%

        \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -145000:\\ \;\;\;\;y \cdot -0.5\\ \mathbf{elif}\;y \leq 1.55:\\ \;\;\;\;0.918938533204673 - x\\ \mathbf{elif}\;y \leq 3.8 \cdot 10^{+208}:\\ \;\;\;\;x \cdot y\\ \mathbf{else}:\\ \;\;\;\;y \cdot -0.5\\ \end{array} \]
      12. Add Preprocessing

      Alternative 5: 49.4% accurate, 0.6× speedup?

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

        1. Initial program 100.0%

          \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
        2. Step-by-step derivation
          1. sub-negN/A

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

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
          3. sub-negN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          4. distribute-lft-inN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          5. associate-+r+N/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          7. associate-+l+N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
          8. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          10. distribute-lft-outN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          11. *-lowering-*.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          13. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          14. metadata-evalN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          15. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
          17. cancel-sign-sub-invN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
          18. *-lft-identityN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
          19. --lowering--.f6499.9%

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
        3. Simplified99.9%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
        4. Add Preprocessing
        5. Taylor expanded in y around inf

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

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

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
          3. metadata-evalN/A

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
          4. +-lowering-+.f6450.7%

            \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
        7. Simplified50.7%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
        8. Taylor expanded in x around inf

          \[\leadsto \color{blue}{x \cdot y} \]
        9. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto y \cdot \color{blue}{x} \]
          2. *-lowering-*.f6450.0%

            \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{x}\right) \]
        10. Simplified50.0%

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

        if -8.49999999999999935e-8 < x < 1.8500000000000001e-190

        1. Initial program 100.0%

          \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
        2. Step-by-step derivation
          1. sub-negN/A

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

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
          3. sub-negN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          4. distribute-lft-inN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          5. associate-+r+N/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
          7. associate-+l+N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
          8. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          10. distribute-lft-outN/A

            \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          11. *-lowering-*.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          12. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          13. +-lowering-+.f64N/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
          14. metadata-evalN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
          15. +-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
          16. *-commutativeN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
          17. cancel-sign-sub-invN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
          18. *-lft-identityN/A

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
          19. --lowering--.f64100.0%

            \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
        3. Simplified100.0%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
        4. Add Preprocessing
        5. Taylor expanded in y around inf

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

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

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
          3. metadata-evalN/A

            \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
          4. +-lowering-+.f6465.2%

            \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
        7. Simplified65.2%

          \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
        8. Taylor expanded in x around 0

          \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{\frac{-1}{2}}\right) \]
        9. Step-by-step derivation
          1. Simplified64.7%

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

          if 1.8500000000000001e-190 < x < 0.71999999999999997

          1. Initial program 100.0%

            \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
          2. Step-by-step derivation
            1. sub-negN/A

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

              \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
            3. sub-negN/A

              \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
            4. distribute-lft-inN/A

              \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
            5. associate-+r+N/A

              \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
            6. *-commutativeN/A

              \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
            7. associate-+l+N/A

              \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
            8. +-lowering-+.f64N/A

              \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
            9. distribute-rgt-neg-inN/A

              \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
            10. distribute-lft-outN/A

              \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
            11. *-lowering-*.f64N/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
            12. +-commutativeN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
            13. +-lowering-+.f64N/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
            14. metadata-evalN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
            15. +-commutativeN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
            16. *-commutativeN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
            17. cancel-sign-sub-invN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
            18. *-lft-identityN/A

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
            19. --lowering--.f64100.0%

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
          3. Simplified100.0%

            \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
          4. Add Preprocessing
          5. Taylor expanded in y around 0

            \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
          6. Step-by-step derivation
            1. --lowering--.f6464.5%

              \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
          7. Simplified64.5%

            \[\leadsto \color{blue}{0.918938533204673 - x} \]
          8. Taylor expanded in x around 0

            \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000}} \]
          9. Step-by-step derivation
            1. Simplified64.0%

              \[\leadsto \color{blue}{0.918938533204673} \]
          10. Recombined 3 regimes into one program.
          11. Final simplification57.4%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -8.5 \cdot 10^{-8}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \leq 1.85 \cdot 10^{-190}:\\ \;\;\;\;y \cdot -0.5\\ \mathbf{elif}\;x \leq 0.72:\\ \;\;\;\;0.918938533204673\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]
          12. Add Preprocessing

          Alternative 6: 98.5% accurate, 0.6× speedup?

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

            1. Initial program 100.0%

              \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
            2. Step-by-step derivation
              1. sub-negN/A

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

                \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
              3. sub-negN/A

                \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
              4. distribute-lft-inN/A

                \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
              5. associate-+r+N/A

                \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
              6. *-commutativeN/A

                \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
              7. associate-+l+N/A

                \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
              8. +-lowering-+.f64N/A

                \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
              9. distribute-rgt-neg-inN/A

                \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
              10. distribute-lft-outN/A

                \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
              11. *-lowering-*.f64N/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
              12. +-commutativeN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
              13. +-lowering-+.f64N/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
              14. metadata-evalN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
              15. +-commutativeN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
              16. *-commutativeN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
              17. cancel-sign-sub-invN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
              18. *-lft-identityN/A

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
              19. --lowering--.f64100.0%

                \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
            3. Simplified100.0%

              \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
            4. Add Preprocessing
            5. Taylor expanded in x around inf

              \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \color{blue}{x}\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, x\right)\right) \]
            6. Step-by-step derivation
              1. Simplified98.3%

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

              if -0.5 < x < 1.9e10

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f64100.0%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified100.0%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in x around 0

                \[\leadsto \mathsf{+.f64}\left(\color{blue}{\left(\frac{-1}{2} \cdot y\right)}, \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, x\right)\right) \]
              6. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{-1}{2}\right), \mathsf{\_.f64}\left(\color{blue}{\frac{918938533204673}{1000000000000000}}, x\right)\right) \]
                2. *-lowering-*.f6499.5%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \frac{-1}{2}\right), \mathsf{\_.f64}\left(\color{blue}{\frac{918938533204673}{1000000000000000}}, x\right)\right) \]
              7. Simplified99.5%

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

              if 1.9e10 < x

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f6499.9%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified99.9%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in x around inf

                \[\leadsto \color{blue}{x \cdot \left(y - 1\right)} \]
              6. Step-by-step derivation
                1. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{\left(y - 1\right)}\right) \]
                2. sub-negN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                3. metadata-evalN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + -1\right)\right) \]
                4. +-lowering-+.f64100.0%

                  \[\leadsto \mathsf{*.f64}\left(x, \mathsf{+.f64}\left(y, \color{blue}{-1}\right)\right) \]
              7. Simplified100.0%

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

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

            Alternative 7: 98.4% accurate, 0.6× speedup?

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

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f6499.9%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified99.9%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in x around inf

                \[\leadsto \color{blue}{x \cdot \left(y - 1\right)} \]
              6. Step-by-step derivation
                1. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{\left(y - 1\right)}\right) \]
                2. sub-negN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                3. metadata-evalN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + -1\right)\right) \]
                4. +-lowering-+.f6498.8%

                  \[\leadsto \mathsf{*.f64}\left(x, \mathsf{+.f64}\left(y, \color{blue}{-1}\right)\right) \]
              7. Simplified98.8%

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

              if -38000 < x < 1.85e10

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f64100.0%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified100.0%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in x around 0

                \[\leadsto \mathsf{+.f64}\left(\color{blue}{\left(\frac{-1}{2} \cdot y\right)}, \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, x\right)\right) \]
              6. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{-1}{2}\right), \mathsf{\_.f64}\left(\color{blue}{\frac{918938533204673}{1000000000000000}}, x\right)\right) \]
                2. *-lowering-*.f6499.5%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \frac{-1}{2}\right), \mathsf{\_.f64}\left(\color{blue}{\frac{918938533204673}{1000000000000000}}, x\right)\right) \]
              7. Simplified99.5%

                \[\leadsto \color{blue}{y \cdot -0.5} + \left(0.918938533204673 - x\right) \]
            3. Recombined 2 regimes into one program.
            4. Final simplification99.2%

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

            Alternative 8: 97.8% accurate, 0.7× speedup?

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

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f6499.9%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified99.9%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in x around inf

                \[\leadsto \color{blue}{x \cdot \left(y - 1\right)} \]
              6. Step-by-step derivation
                1. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{\left(y - 1\right)}\right) \]
                2. sub-negN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                3. metadata-evalN/A

                  \[\leadsto \mathsf{*.f64}\left(x, \left(y + -1\right)\right) \]
                4. +-lowering-+.f6497.9%

                  \[\leadsto \mathsf{*.f64}\left(x, \mathsf{+.f64}\left(y, \color{blue}{-1}\right)\right) \]
              7. Simplified97.9%

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

              if -0.75 < x < 0.52000000000000002

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

                \[\leadsto \mathsf{+.f64}\left(\color{blue}{\left(\frac{-1}{2} \cdot y\right)}, \frac{918938533204673}{1000000000000000}\right) \]
              4. Step-by-step derivation
                1. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{-1}{2}\right), \frac{918938533204673}{1000000000000000}\right) \]
                2. *-lowering-*.f6498.2%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \frac{-1}{2}\right), \frac{918938533204673}{1000000000000000}\right) \]
              5. Simplified98.2%

                \[\leadsto \color{blue}{y \cdot -0.5} + 0.918938533204673 \]
            3. Recombined 2 regimes into one program.
            4. Final simplification98.1%

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

            Alternative 9: 49.6% accurate, 0.8× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;y \leq -0.75:\\ \;\;\;\;y \cdot -0.5\\ \mathbf{elif}\;y \leq 0.95:\\ \;\;\;\;0.918938533204673\\ \mathbf{else}:\\ \;\;\;\;y \cdot -0.5\\ \end{array} \end{array} \]
            (FPCore (x y)
             :precision binary64
             (if (<= y -0.75) (* y -0.5) (if (<= y 0.95) 0.918938533204673 (* y -0.5))))
            double code(double x, double y) {
            	double tmp;
            	if (y <= -0.75) {
            		tmp = y * -0.5;
            	} else if (y <= 0.95) {
            		tmp = 0.918938533204673;
            	} else {
            		tmp = y * -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 <= (-0.75d0)) then
                    tmp = y * (-0.5d0)
                else if (y <= 0.95d0) then
                    tmp = 0.918938533204673d0
                else
                    tmp = y * (-0.5d0)
                end if
                code = tmp
            end function
            
            public static double code(double x, double y) {
            	double tmp;
            	if (y <= -0.75) {
            		tmp = y * -0.5;
            	} else if (y <= 0.95) {
            		tmp = 0.918938533204673;
            	} else {
            		tmp = y * -0.5;
            	}
            	return tmp;
            }
            
            def code(x, y):
            	tmp = 0
            	if y <= -0.75:
            		tmp = y * -0.5
            	elif y <= 0.95:
            		tmp = 0.918938533204673
            	else:
            		tmp = y * -0.5
            	return tmp
            
            function code(x, y)
            	tmp = 0.0
            	if (y <= -0.75)
            		tmp = Float64(y * -0.5);
            	elseif (y <= 0.95)
            		tmp = 0.918938533204673;
            	else
            		tmp = Float64(y * -0.5);
            	end
            	return tmp
            end
            
            function tmp_2 = code(x, y)
            	tmp = 0.0;
            	if (y <= -0.75)
            		tmp = y * -0.5;
            	elseif (y <= 0.95)
            		tmp = 0.918938533204673;
            	else
            		tmp = y * -0.5;
            	end
            	tmp_2 = tmp;
            end
            
            code[x_, y_] := If[LessEqual[y, -0.75], N[(y * -0.5), $MachinePrecision], If[LessEqual[y, 0.95], 0.918938533204673, N[(y * -0.5), $MachinePrecision]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            \mathbf{if}\;y \leq -0.75:\\
            \;\;\;\;y \cdot -0.5\\
            
            \mathbf{elif}\;y \leq 0.95:\\
            \;\;\;\;0.918938533204673\\
            
            \mathbf{else}:\\
            \;\;\;\;y \cdot -0.5\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if y < -0.75 or 0.94999999999999996 < y

              1. Initial program 100.0%

                \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
              2. Step-by-step derivation
                1. sub-negN/A

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

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                3. sub-negN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                4. distribute-lft-inN/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                5. associate-+r+N/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                6. *-commutativeN/A

                  \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                7. associate-+l+N/A

                  \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                8. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                9. distribute-rgt-neg-inN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                10. distribute-lft-outN/A

                  \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                11. *-lowering-*.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                13. +-lowering-+.f64N/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                14. metadata-evalN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                15. +-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                16. *-commutativeN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                17. cancel-sign-sub-invN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                18. *-lft-identityN/A

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                19. --lowering--.f6499.9%

                  \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
              3. Simplified99.9%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
              4. Add Preprocessing
              5. Taylor expanded in y around inf

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

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

                  \[\leadsto \mathsf{*.f64}\left(y, \left(x + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{2}\right)\right)}\right)\right) \]
                3. metadata-evalN/A

                  \[\leadsto \mathsf{*.f64}\left(y, \left(x + \frac{-1}{2}\right)\right) \]
                4. +-lowering-+.f6496.2%

                  \[\leadsto \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right) \]
              7. Simplified96.2%

                \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right)} \]
              8. Taylor expanded in x around 0

                \[\leadsto \mathsf{*.f64}\left(y, \color{blue}{\frac{-1}{2}}\right) \]
              9. Step-by-step derivation
                1. Simplified53.3%

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

                if -0.75 < y < 0.94999999999999996

                1. Initial program 100.0%

                  \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
                2. Step-by-step derivation
                  1. sub-negN/A

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

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  3. sub-negN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  4. distribute-lft-inN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  5. associate-+r+N/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  6. *-commutativeN/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  7. associate-+l+N/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                  8. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                  9. distribute-rgt-neg-inN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  10. distribute-lft-outN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  11. *-lowering-*.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  12. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  13. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  14. metadata-evalN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  15. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                  16. *-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                  17. cancel-sign-sub-invN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                  18. *-lft-identityN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                  19. --lowering--.f64100.0%

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
                3. Simplified100.0%

                  \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
                4. Add Preprocessing
                5. Taylor expanded in y around 0

                  \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
                6. Step-by-step derivation
                  1. --lowering--.f6495.7%

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
                7. Simplified95.7%

                  \[\leadsto \color{blue}{0.918938533204673 - x} \]
                8. Taylor expanded in x around 0

                  \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000}} \]
                9. Step-by-step derivation
                  1. Simplified50.3%

                    \[\leadsto \color{blue}{0.918938533204673} \]
                10. Recombined 2 regimes into one program.
                11. Add Preprocessing

                Alternative 10: 100.0% accurate, 1.2× speedup?

                \[\begin{array}{l} \\ 0.918938533204673 + \left(y \cdot \left(x + -0.5\right) - x\right) \end{array} \]
                (FPCore (x y) :precision binary64 (+ 0.918938533204673 (- (* y (+ x -0.5)) x)))
                double code(double x, double y) {
                	return 0.918938533204673 + ((y * (x + -0.5)) - x);
                }
                
                real(8) function code(x, y)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    code = 0.918938533204673d0 + ((y * (x + (-0.5d0))) - x)
                end function
                
                public static double code(double x, double y) {
                	return 0.918938533204673 + ((y * (x + -0.5)) - x);
                }
                
                def code(x, y):
                	return 0.918938533204673 + ((y * (x + -0.5)) - x)
                
                function code(x, y)
                	return Float64(0.918938533204673 + Float64(Float64(y * Float64(x + -0.5)) - x))
                end
                
                function tmp = code(x, y)
                	tmp = 0.918938533204673 + ((y * (x + -0.5)) - x);
                end
                
                code[x_, y_] := N[(0.918938533204673 + N[(N[(y * N[(x + -0.5), $MachinePrecision]), $MachinePrecision] - x), $MachinePrecision]), $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                0.918938533204673 + \left(y \cdot \left(x + -0.5\right) - x\right)
                \end{array}
                
                Derivation
                1. Initial program 100.0%

                  \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
                2. Step-by-step derivation
                  1. sub-negN/A

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

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  3. sub-negN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  4. distribute-lft-inN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  5. associate-+r+N/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  6. *-commutativeN/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  7. associate-+l+N/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                  8. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                  9. distribute-rgt-neg-inN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  10. distribute-lft-outN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  11. *-lowering-*.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  12. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  13. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  14. metadata-evalN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  15. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                  16. *-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                  17. cancel-sign-sub-invN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                  18. *-lft-identityN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                  19. --lowering--.f64100.0%

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
                3. Simplified100.0%

                  \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
                4. Add Preprocessing
                5. Step-by-step derivation
                  1. +-commutativeN/A

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

                    \[\leadsto \frac{918938533204673}{1000000000000000} - \color{blue}{\left(x - y \cdot \left(x + \frac{-1}{2}\right)\right)} \]
                  3. --lowering--.f64N/A

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{\left(x - y \cdot \left(x + \frac{-1}{2}\right)\right)}\right) \]
                  4. --lowering--.f64N/A

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \mathsf{\_.f64}\left(x, \color{blue}{\left(y \cdot \left(x + \frac{-1}{2}\right)\right)}\right)\right) \]
                  5. *-lowering-*.f64N/A

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, \color{blue}{\left(x + \frac{-1}{2}\right)}\right)\right)\right) \]
                  6. +-lowering-+.f64100.0%

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right)\right)\right)\right) \]
                6. Applied egg-rr100.0%

                  \[\leadsto \color{blue}{0.918938533204673 - \left(x - y \cdot \left(x + -0.5\right)\right)} \]
                7. Final simplification100.0%

                  \[\leadsto 0.918938533204673 + \left(y \cdot \left(x + -0.5\right) - x\right) \]
                8. Add Preprocessing

                Alternative 11: 100.0% accurate, 1.2× speedup?

                \[\begin{array}{l} \\ y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right) \end{array} \]
                (FPCore (x y) :precision binary64 (+ (* y (+ x -0.5)) (- 0.918938533204673 x)))
                double code(double x, double y) {
                	return (y * (x + -0.5)) + (0.918938533204673 - x);
                }
                
                real(8) function code(x, y)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    code = (y * (x + (-0.5d0))) + (0.918938533204673d0 - x)
                end function
                
                public static double code(double x, double y) {
                	return (y * (x + -0.5)) + (0.918938533204673 - x);
                }
                
                def code(x, y):
                	return (y * (x + -0.5)) + (0.918938533204673 - x)
                
                function code(x, y)
                	return Float64(Float64(y * Float64(x + -0.5)) + Float64(0.918938533204673 - x))
                end
                
                function tmp = code(x, y)
                	tmp = (y * (x + -0.5)) + (0.918938533204673 - x);
                end
                
                code[x_, y_] := N[(N[(y * N[(x + -0.5), $MachinePrecision]), $MachinePrecision] + N[(0.918938533204673 - x), $MachinePrecision]), $MachinePrecision]
                
                \begin{array}{l}
                
                \\
                y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)
                \end{array}
                
                Derivation
                1. Initial program 100.0%

                  \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
                2. Step-by-step derivation
                  1. sub-negN/A

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

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  3. sub-negN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  4. distribute-lft-inN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  5. associate-+r+N/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  6. *-commutativeN/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  7. associate-+l+N/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                  8. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                  9. distribute-rgt-neg-inN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  10. distribute-lft-outN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  11. *-lowering-*.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  12. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  13. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  14. metadata-evalN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  15. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                  16. *-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                  17. cancel-sign-sub-invN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                  18. *-lft-identityN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                  19. --lowering--.f64100.0%

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
                3. Simplified100.0%

                  \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
                4. Add Preprocessing
                5. Add Preprocessing

                Alternative 12: 26.3% accurate, 11.0× speedup?

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

                  \[\left(x \cdot \left(y - 1\right) - y \cdot 0.5\right) + 0.918938533204673 \]
                2. Step-by-step derivation
                  1. sub-negN/A

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

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y - 1\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  3. sub-negN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot \left(y + \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  4. distribute-lft-inN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + \left(x \cdot y + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  5. associate-+r+N/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + x \cdot y\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  6. *-commutativeN/A

                    \[\leadsto \left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + x \cdot \left(\mathsf{neg}\left(1\right)\right)\right) + \frac{918938533204673}{1000000000000000} \]
                  7. associate-+l+N/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right) + \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)} \]
                  8. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\left(\left(\mathsf{neg}\left(y \cdot \frac{1}{2}\right)\right) + y \cdot x\right), \color{blue}{\left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)}\right) \]
                  9. distribute-rgt-neg-inN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + y \cdot x\right), \left(\color{blue}{x} \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  10. distribute-lft-outN/A

                    \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  11. *-lowering-*.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) + x\right)\right), \left(\color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  12. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \left(x + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  13. +-lowering-+.f64N/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right), \left(x \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)} + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  14. metadata-evalN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(x \cdot \left(\mathsf{neg}\left(1\right)\right) + \frac{918938533204673}{1000000000000000}\right)\right) \]
                  15. +-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \color{blue}{x \cdot \left(\mathsf{neg}\left(1\right)\right)}\right)\right) \]
                  16. *-commutativeN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} + \left(\mathsf{neg}\left(1\right)\right) \cdot \color{blue}{x}\right)\right) \]
                  17. cancel-sign-sub-invN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - \color{blue}{1 \cdot x}\right)\right) \]
                  18. *-lft-identityN/A

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \left(\frac{918938533204673}{1000000000000000} - x\right)\right) \]
                  19. --lowering--.f64100.0%

                    \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(y, \mathsf{+.f64}\left(x, \frac{-1}{2}\right)\right), \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right)\right) \]
                3. Simplified100.0%

                  \[\leadsto \color{blue}{y \cdot \left(x + -0.5\right) + \left(0.918938533204673 - x\right)} \]
                4. Add Preprocessing
                5. Taylor expanded in y around 0

                  \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000} - x} \]
                6. Step-by-step derivation
                  1. --lowering--.f6445.8%

                    \[\leadsto \mathsf{\_.f64}\left(\frac{918938533204673}{1000000000000000}, \color{blue}{x}\right) \]
                7. Simplified45.8%

                  \[\leadsto \color{blue}{0.918938533204673 - x} \]
                8. Taylor expanded in x around 0

                  \[\leadsto \color{blue}{\frac{918938533204673}{1000000000000000}} \]
                9. Step-by-step derivation
                  1. Simplified24.5%

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

                  Reproduce

                  ?
                  herbie shell --seed 2024155 
                  (FPCore (x y)
                    :name "Numeric.SpecFunctions:logGamma from math-functions-0.1.5.2, A"
                    :precision binary64
                    (+ (- (* x (- y 1.0)) (* y 0.5)) 0.918938533204673))