Numeric.LinearAlgebra.Util:formatSparse from hmatrix-0.16.1.5

Percentage Accurate: 100.0% → 100.0%
Time: 6.9s
Alternatives: 6
Speedup: 1.1×

Specification

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

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

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

Alternative 1: 100.0% accurate, 1.1× speedup?

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

\\
\left|\frac{y - x}{y}\right|
\end{array}
Derivation
  1. Initial program 100.0%

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

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

      \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
    3. neg-fabsN/A

      \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
    4. lift-fabs.f64N/A

      \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
    5. div-fabsN/A

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

      \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
    7. lower-/.f64N/A

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

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

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

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

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

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

      \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    14. lower--.f64100.0

      \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
  4. Applied rewrites100.0%

    \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
  5. Add Preprocessing

Alternative 2: 99.1% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\ \;\;\;\;1 - \frac{x}{y}\\ \mathbf{else}:\\ \;\;\;\;\left|\frac{-x}{y}\right|\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (if (<= (fabs (/ (- y x) y)) 50000000.0) (- 1.0 (/ x y)) (fabs (/ (- x) y))))
double code(double x, double y) {
	double tmp;
	if (fabs(((y - x) / y)) <= 50000000.0) {
		tmp = 1.0 - (x / y);
	} else {
		tmp = fabs((-x / y));
	}
	return tmp;
}
real(8) function code(x, y)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8) :: tmp
    if (abs(((y - x) / y)) <= 50000000.0d0) then
        tmp = 1.0d0 - (x / y)
    else
        tmp = abs((-x / y))
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double tmp;
	if (Math.abs(((y - x) / y)) <= 50000000.0) {
		tmp = 1.0 - (x / y);
	} else {
		tmp = Math.abs((-x / y));
	}
	return tmp;
}
def code(x, y):
	tmp = 0
	if math.fabs(((y - x) / y)) <= 50000000.0:
		tmp = 1.0 - (x / y)
	else:
		tmp = math.fabs((-x / y))
	return tmp
function code(x, y)
	tmp = 0.0
	if (abs(Float64(Float64(y - x) / y)) <= 50000000.0)
		tmp = Float64(1.0 - Float64(x / y));
	else
		tmp = abs(Float64(Float64(-x) / y));
	end
	return tmp
end
function tmp_2 = code(x, y)
	tmp = 0.0;
	if (abs(((y - x) / y)) <= 50000000.0)
		tmp = 1.0 - (x / y);
	else
		tmp = abs((-x / y));
	end
	tmp_2 = tmp;
end
code[x_, y_] := If[LessEqual[N[Abs[N[(N[(y - x), $MachinePrecision] / y), $MachinePrecision]], $MachinePrecision], 50000000.0], N[(1.0 - N[(x / y), $MachinePrecision]), $MachinePrecision], N[Abs[N[((-x) / y), $MachinePrecision]], $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\
\;\;\;\;1 - \frac{x}{y}\\

\mathbf{else}:\\
\;\;\;\;\left|\frac{-x}{y}\right|\\


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

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

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

        \[\leadsto \frac{\color{blue}{y - x}}{y} \]
      13. div-subN/A

        \[\leadsto \color{blue}{\frac{y}{y} - \frac{x}{y}} \]
      14. *-inversesN/A

        \[\leadsto \color{blue}{1} - \frac{x}{y} \]
      15. lower--.f64N/A

        \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
      16. lower-/.f6498.6

        \[\leadsto 1 - \color{blue}{\frac{x}{y}} \]
    6. Applied rewrites98.6%

      \[\leadsto \color{blue}{1 - \frac{x}{y}} \]

    if 5e7 < (/.f64 (fabs.f64 (-.f64 x y)) (fabs.f64 y))

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Taylor expanded in y around 0

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

        \[\leadsto \left|\frac{\color{blue}{\mathsf{neg}\left(x\right)}}{y}\right| \]
      2. lower-neg.f6499.6

        \[\leadsto \left|\frac{\color{blue}{-x}}{y}\right| \]
    7. Applied rewrites99.6%

      \[\leadsto \left|\frac{\color{blue}{-x}}{y}\right| \]
  3. Recombined 2 regimes into one program.
  4. Final simplification99.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\ \;\;\;\;1 - \frac{x}{y}\\ \mathbf{else}:\\ \;\;\;\;\left|\frac{-x}{y}\right|\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 74.1% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\ \;\;\;\;1 - \frac{x}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{y} - 1\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (if (<= (fabs (/ (- y x) y)) 50000000.0) (- 1.0 (/ x y)) (- (/ x y) 1.0)))
double code(double x, double y) {
	double tmp;
	if (fabs(((y - x) / y)) <= 50000000.0) {
		tmp = 1.0 - (x / y);
	} 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 (abs(((y - x) / y)) <= 50000000.0d0) then
        tmp = 1.0d0 - (x / y)
    else
        tmp = (x / y) - 1.0d0
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double tmp;
	if (Math.abs(((y - x) / y)) <= 50000000.0) {
		tmp = 1.0 - (x / y);
	} else {
		tmp = (x / y) - 1.0;
	}
	return tmp;
}
def code(x, y):
	tmp = 0
	if math.fabs(((y - x) / y)) <= 50000000.0:
		tmp = 1.0 - (x / y)
	else:
		tmp = (x / y) - 1.0
	return tmp
function code(x, y)
	tmp = 0.0
	if (abs(Float64(Float64(y - x) / y)) <= 50000000.0)
		tmp = Float64(1.0 - Float64(x / y));
	else
		tmp = Float64(Float64(x / y) - 1.0);
	end
	return tmp
end
function tmp_2 = code(x, y)
	tmp = 0.0;
	if (abs(((y - x) / y)) <= 50000000.0)
		tmp = 1.0 - (x / y);
	else
		tmp = (x / y) - 1.0;
	end
	tmp_2 = tmp;
end
code[x_, y_] := If[LessEqual[N[Abs[N[(N[(y - x), $MachinePrecision] / y), $MachinePrecision]], $MachinePrecision], 50000000.0], N[(1.0 - N[(x / y), $MachinePrecision]), $MachinePrecision], N[(N[(x / y), $MachinePrecision] - 1.0), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\
\;\;\;\;1 - \frac{x}{y}\\

\mathbf{else}:\\
\;\;\;\;\frac{x}{y} - 1\\


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

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

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

        \[\leadsto \frac{\color{blue}{y - x}}{y} \]
      13. div-subN/A

        \[\leadsto \color{blue}{\frac{y}{y} - \frac{x}{y}} \]
      14. *-inversesN/A

        \[\leadsto \color{blue}{1} - \frac{x}{y} \]
      15. lower--.f64N/A

        \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
      16. lower-/.f6498.6

        \[\leadsto 1 - \color{blue}{\frac{x}{y}} \]
    6. Applied rewrites98.6%

      \[\leadsto \color{blue}{1 - \frac{x}{y}} \]

    if 5e7 < (/.f64 (fabs.f64 (-.f64 x y)) (fabs.f64 y))

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

        \[\leadsto \color{blue}{\frac{y - x}{y}} \]
      12. frac-2negN/A

        \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(y - x\right)\right)}{\mathsf{neg}\left(y\right)}} \]
      13. div-invN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y - x\right)\right)\right) \cdot \frac{1}{\mathsf{neg}\left(y\right)}} \]
      14. lift--.f64N/A

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

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

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

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

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

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{1}{\mathsf{neg}\left(y\right)} \]
      20. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}} \]
      21. sqr-powN/A

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

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

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}}\right| \]
      24. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{\frac{1}{\mathsf{neg}\left(y\right)}}\right| \]
      25. fabs-divN/A

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

        \[\leadsto \left(x - y\right) \cdot \frac{\left|1\right|}{\color{blue}{\left|y\right|}} \]
      27. fabs-divN/A

        \[\leadsto \left(x - y\right) \cdot \color{blue}{\left|\frac{1}{y}\right|} \]
      28. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{y}^{-1}}\right| \]
      29. sqr-powN/A

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

      \[\leadsto \color{blue}{\frac{x}{y} - 1} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification79.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 50000000:\\ \;\;\;\;1 - \frac{x}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{y} - 1\\ \end{array} \]
  5. Add Preprocessing

Alternative 4: 74.2% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 4 \cdot 10^{+19}:\\ \;\;\;\;1 - \frac{x}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{y}\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (if (<= (fabs (/ (- y x) y)) 4e+19) (- 1.0 (/ x y)) (/ x y)))
double code(double x, double y) {
	double tmp;
	if (fabs(((y - x) / y)) <= 4e+19) {
		tmp = 1.0 - (x / y);
	} 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 (abs(((y - x) / y)) <= 4d+19) then
        tmp = 1.0d0 - (x / y)
    else
        tmp = x / y
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double tmp;
	if (Math.abs(((y - x) / y)) <= 4e+19) {
		tmp = 1.0 - (x / y);
	} else {
		tmp = x / y;
	}
	return tmp;
}
def code(x, y):
	tmp = 0
	if math.fabs(((y - x) / y)) <= 4e+19:
		tmp = 1.0 - (x / y)
	else:
		tmp = x / y
	return tmp
function code(x, y)
	tmp = 0.0
	if (abs(Float64(Float64(y - x) / y)) <= 4e+19)
		tmp = Float64(1.0 - Float64(x / y));
	else
		tmp = Float64(x / y);
	end
	return tmp
end
function tmp_2 = code(x, y)
	tmp = 0.0;
	if (abs(((y - x) / y)) <= 4e+19)
		tmp = 1.0 - (x / y);
	else
		tmp = x / y;
	end
	tmp_2 = tmp;
end
code[x_, y_] := If[LessEqual[N[Abs[N[(N[(y - x), $MachinePrecision] / y), $MachinePrecision]], $MachinePrecision], 4e+19], N[(1.0 - N[(x / y), $MachinePrecision]), $MachinePrecision], N[(x / y), $MachinePrecision]]
\begin{array}{l}

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

\mathbf{else}:\\
\;\;\;\;\frac{x}{y}\\


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

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

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

        \[\leadsto \frac{\color{blue}{y - x}}{y} \]
      13. div-subN/A

        \[\leadsto \color{blue}{\frac{y}{y} - \frac{x}{y}} \]
      14. *-inversesN/A

        \[\leadsto \color{blue}{1} - \frac{x}{y} \]
      15. lower--.f64N/A

        \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
      16. lower-/.f6497.2

        \[\leadsto 1 - \color{blue}{\frac{x}{y}} \]
    6. Applied rewrites97.2%

      \[\leadsto \color{blue}{1 - \frac{x}{y}} \]

    if 4e19 < (/.f64 (fabs.f64 (-.f64 x y)) (fabs.f64 y))

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

        \[\leadsto \color{blue}{\frac{y - x}{y}} \]
      12. frac-2negN/A

        \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(y - x\right)\right)}{\mathsf{neg}\left(y\right)}} \]
      13. div-invN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y - x\right)\right)\right) \cdot \frac{1}{\mathsf{neg}\left(y\right)}} \]
      14. lift--.f64N/A

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

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

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

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

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

        \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{1}{\mathsf{neg}\left(y\right)} \]
      20. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}} \]
      21. sqr-powN/A

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

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

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}}\right| \]
      24. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{\frac{1}{\mathsf{neg}\left(y\right)}}\right| \]
      25. fabs-divN/A

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

        \[\leadsto \left(x - y\right) \cdot \frac{\left|1\right|}{\color{blue}{\left|y\right|}} \]
      27. fabs-divN/A

        \[\leadsto \left(x - y\right) \cdot \color{blue}{\left|\frac{1}{y}\right|} \]
      28. inv-powN/A

        \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{y}^{-1}}\right| \]
      29. sqr-powN/A

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

      \[\leadsto \color{blue}{\frac{x}{y} - 1} \]
    7. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{x}{y}} \]
    8. Step-by-step derivation
      1. lower-/.f6458.1

        \[\leadsto \color{blue}{\frac{x}{y}} \]
    9. Applied rewrites58.1%

      \[\leadsto \color{blue}{\frac{x}{y}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification79.8%

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

Alternative 5: 72.4% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 4500:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{y}\\ \end{array} \end{array} \]
(FPCore (x y)
 :precision binary64
 (if (<= (fabs (/ (- y x) y)) 4500.0) 1.0 (/ x y)))
double code(double x, double y) {
	double tmp;
	if (fabs(((y - x) / y)) <= 4500.0) {
		tmp = 1.0;
	} 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 (abs(((y - x) / y)) <= 4500.0d0) then
        tmp = 1.0d0
    else
        tmp = x / y
    end if
    code = tmp
end function
public static double code(double x, double y) {
	double tmp;
	if (Math.abs(((y - x) / y)) <= 4500.0) {
		tmp = 1.0;
	} else {
		tmp = x / y;
	}
	return tmp;
}
def code(x, y):
	tmp = 0
	if math.fabs(((y - x) / y)) <= 4500.0:
		tmp = 1.0
	else:
		tmp = x / y
	return tmp
function code(x, y)
	tmp = 0.0
	if (abs(Float64(Float64(y - x) / y)) <= 4500.0)
		tmp = 1.0;
	else
		tmp = Float64(x / y);
	end
	return tmp
end
function tmp_2 = code(x, y)
	tmp = 0.0;
	if (abs(((y - x) / y)) <= 4500.0)
		tmp = 1.0;
	else
		tmp = x / y;
	end
	tmp_2 = tmp;
end
code[x_, y_] := If[LessEqual[N[Abs[N[(N[(y - x), $MachinePrecision] / y), $MachinePrecision]], $MachinePrecision], 4500.0], 1.0, N[(x / y), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 4500:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\frac{x}{y}\\


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

    1. Initial program 100.0%

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

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

        \[\leadsto \frac{\color{blue}{y - x}}{y} \]
      13. div-subN/A

        \[\leadsto \color{blue}{\frac{y}{y} - \frac{x}{y}} \]
      14. *-inversesN/A

        \[\leadsto \color{blue}{1} - \frac{x}{y} \]
      15. lower--.f64N/A

        \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
      16. lower-/.f6499.3

        \[\leadsto 1 - \color{blue}{\frac{x}{y}} \]
    6. Applied rewrites99.3%

      \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
    7. Taylor expanded in y around inf

      \[\leadsto \color{blue}{1} \]
    8. Step-by-step derivation
      1. Applied rewrites96.5%

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

      if 4500 < (/.f64 (fabs.f64 (-.f64 x y)) (fabs.f64 y))

      1. Initial program 100.0%

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

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

          \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
        3. neg-fabsN/A

          \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
        4. lift-fabs.f64N/A

          \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
        5. div-fabsN/A

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

          \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
        7. lower-/.f64N/A

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

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

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

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

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

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

          \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
        14. lower--.f64100.0

          \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      4. Applied rewrites100.0%

        \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
      5. Step-by-step derivation
        1. lift-fabs.f64N/A

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

          \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
        3. clear-numN/A

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

          \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
        5. inv-powN/A

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

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

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

          \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
        9. inv-powN/A

          \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
        10. lift-/.f64N/A

          \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
        11. clear-numN/A

          \[\leadsto \color{blue}{\frac{y - x}{y}} \]
        12. frac-2negN/A

          \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(y - x\right)\right)}{\mathsf{neg}\left(y\right)}} \]
        13. div-invN/A

          \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(y - x\right)\right)\right) \cdot \frac{1}{\mathsf{neg}\left(y\right)}} \]
        14. lift--.f64N/A

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

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

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

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

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

          \[\leadsto \color{blue}{\left(x - y\right)} \cdot \frac{1}{\mathsf{neg}\left(y\right)} \]
        20. inv-powN/A

          \[\leadsto \left(x - y\right) \cdot \color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}} \]
        21. sqr-powN/A

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

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

          \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{\left(\mathsf{neg}\left(y\right)\right)}^{-1}}\right| \]
        24. inv-powN/A

          \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{\frac{1}{\mathsf{neg}\left(y\right)}}\right| \]
        25. fabs-divN/A

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

          \[\leadsto \left(x - y\right) \cdot \frac{\left|1\right|}{\color{blue}{\left|y\right|}} \]
        27. fabs-divN/A

          \[\leadsto \left(x - y\right) \cdot \color{blue}{\left|\frac{1}{y}\right|} \]
        28. inv-powN/A

          \[\leadsto \left(x - y\right) \cdot \left|\color{blue}{{y}^{-1}}\right| \]
        29. sqr-powN/A

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

        \[\leadsto \color{blue}{\frac{x}{y} - 1} \]
      7. Taylor expanded in y around 0

        \[\leadsto \color{blue}{\frac{x}{y}} \]
      8. Step-by-step derivation
        1. lower-/.f6456.3

          \[\leadsto \color{blue}{\frac{x}{y}} \]
      9. Applied rewrites56.3%

        \[\leadsto \color{blue}{\frac{x}{y}} \]
    9. Recombined 2 regimes into one program.
    10. Final simplification77.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left|\frac{y - x}{y}\right| \leq 4500:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{y}\\ \end{array} \]
    11. Add Preprocessing

    Alternative 6: 51.1% accurate, 19.0× speedup?

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

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

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

        \[\leadsto \frac{\color{blue}{\left|x - y\right|}}{\left|y\right|} \]
      3. neg-fabsN/A

        \[\leadsto \frac{\color{blue}{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}}{\left|y\right|} \]
      4. lift-fabs.f64N/A

        \[\leadsto \frac{\left|\mathsf{neg}\left(\left(x - y\right)\right)\right|}{\color{blue}{\left|y\right|}} \]
      5. div-fabsN/A

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

        \[\leadsto \color{blue}{\left|\frac{\mathsf{neg}\left(\left(x - y\right)\right)}{y}\right|} \]
      7. lower-/.f64N/A

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

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

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

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

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

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

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
      14. lower--.f64100.0

        \[\leadsto \left|\frac{\color{blue}{y - x}}{y}\right| \]
    4. Applied rewrites100.0%

      \[\leadsto \color{blue}{\left|\frac{y - x}{y}\right|} \]
    5. Step-by-step derivation
      1. lift-fabs.f64N/A

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

        \[\leadsto \left|\color{blue}{\frac{y - x}{y}}\right| \]
      3. clear-numN/A

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

        \[\leadsto \left|\frac{1}{\color{blue}{\frac{y}{y - x}}}\right| \]
      5. inv-powN/A

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

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

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

        \[\leadsto \color{blue}{{\left(\frac{y}{y - x}\right)}^{-1}} \]
      9. inv-powN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{y}{y - x}}} \]
      10. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{y}{y - x}}} \]
      11. clear-numN/A

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

        \[\leadsto \frac{\color{blue}{y - x}}{y} \]
      13. div-subN/A

        \[\leadsto \color{blue}{\frac{y}{y} - \frac{x}{y}} \]
      14. *-inversesN/A

        \[\leadsto \color{blue}{1} - \frac{x}{y} \]
      15. lower--.f64N/A

        \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
      16. lower-/.f6472.8

        \[\leadsto 1 - \color{blue}{\frac{x}{y}} \]
    6. Applied rewrites72.8%

      \[\leadsto \color{blue}{1 - \frac{x}{y}} \]
    7. Taylor expanded in y around inf

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

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

      Reproduce

      ?
      herbie shell --seed 2024277 
      (FPCore (x y)
        :name "Numeric.LinearAlgebra.Util:formatSparse from hmatrix-0.16.1.5"
        :precision binary64
        (/ (fabs (- x y)) (fabs y)))