Average Error: 29.4 → 0.0
Time: 8.5s
Precision: binary64
Cost: 1096
\[\frac{x}{x + 1} - \frac{x + 1}{x - 1} \]
\[\begin{array}{l} \mathbf{if}\;x \leq -4000000000:\\ \;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\ \mathbf{elif}\;x \leq 2 \cdot 10^{+14}:\\ \;\;\;\;\frac{-1 + -3 \cdot x}{\left(1 - x\right) \cdot \left(-1 - x\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-3}{x}\\ \end{array} \]
(FPCore (x) :precision binary64 (- (/ x (+ x 1.0)) (/ (+ x 1.0) (- x 1.0))))
(FPCore (x)
 :precision binary64
 (if (<= x -4000000000.0)
   (/ (+ -3.0 (/ -1.0 x)) x)
   (if (<= x 2e+14)
     (/ (+ -1.0 (* -3.0 x)) (* (- 1.0 x) (- -1.0 x)))
     (/ -3.0 x))))
double code(double x) {
	return (x / (x + 1.0)) - ((x + 1.0) / (x - 1.0));
}
double code(double x) {
	double tmp;
	if (x <= -4000000000.0) {
		tmp = (-3.0 + (-1.0 / x)) / x;
	} else if (x <= 2e+14) {
		tmp = (-1.0 + (-3.0 * x)) / ((1.0 - x) * (-1.0 - x));
	} else {
		tmp = -3.0 / x;
	}
	return tmp;
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = (x / (x + 1.0d0)) - ((x + 1.0d0) / (x - 1.0d0))
end function
real(8) function code(x)
    real(8), intent (in) :: x
    real(8) :: tmp
    if (x <= (-4000000000.0d0)) then
        tmp = ((-3.0d0) + ((-1.0d0) / x)) / x
    else if (x <= 2d+14) then
        tmp = ((-1.0d0) + ((-3.0d0) * x)) / ((1.0d0 - x) * ((-1.0d0) - x))
    else
        tmp = (-3.0d0) / x
    end if
    code = tmp
end function
public static double code(double x) {
	return (x / (x + 1.0)) - ((x + 1.0) / (x - 1.0));
}
public static double code(double x) {
	double tmp;
	if (x <= -4000000000.0) {
		tmp = (-3.0 + (-1.0 / x)) / x;
	} else if (x <= 2e+14) {
		tmp = (-1.0 + (-3.0 * x)) / ((1.0 - x) * (-1.0 - x));
	} else {
		tmp = -3.0 / x;
	}
	return tmp;
}
def code(x):
	return (x / (x + 1.0)) - ((x + 1.0) / (x - 1.0))
def code(x):
	tmp = 0
	if x <= -4000000000.0:
		tmp = (-3.0 + (-1.0 / x)) / x
	elif x <= 2e+14:
		tmp = (-1.0 + (-3.0 * x)) / ((1.0 - x) * (-1.0 - x))
	else:
		tmp = -3.0 / x
	return tmp
function code(x)
	return Float64(Float64(x / Float64(x + 1.0)) - Float64(Float64(x + 1.0) / Float64(x - 1.0)))
end
function code(x)
	tmp = 0.0
	if (x <= -4000000000.0)
		tmp = Float64(Float64(-3.0 + Float64(-1.0 / x)) / x);
	elseif (x <= 2e+14)
		tmp = Float64(Float64(-1.0 + Float64(-3.0 * x)) / Float64(Float64(1.0 - x) * Float64(-1.0 - x)));
	else
		tmp = Float64(-3.0 / x);
	end
	return tmp
end
function tmp = code(x)
	tmp = (x / (x + 1.0)) - ((x + 1.0) / (x - 1.0));
end
function tmp_2 = code(x)
	tmp = 0.0;
	if (x <= -4000000000.0)
		tmp = (-3.0 + (-1.0 / x)) / x;
	elseif (x <= 2e+14)
		tmp = (-1.0 + (-3.0 * x)) / ((1.0 - x) * (-1.0 - x));
	else
		tmp = -3.0 / x;
	end
	tmp_2 = tmp;
end
code[x_] := N[(N[(x / N[(x + 1.0), $MachinePrecision]), $MachinePrecision] - N[(N[(x + 1.0), $MachinePrecision] / N[(x - 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_] := If[LessEqual[x, -4000000000.0], N[(N[(-3.0 + N[(-1.0 / x), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision], If[LessEqual[x, 2e+14], N[(N[(-1.0 + N[(-3.0 * x), $MachinePrecision]), $MachinePrecision] / N[(N[(1.0 - x), $MachinePrecision] * N[(-1.0 - x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(-3.0 / x), $MachinePrecision]]]
\frac{x}{x + 1} - \frac{x + 1}{x - 1}
\begin{array}{l}
\mathbf{if}\;x \leq -4000000000:\\
\;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\

\mathbf{elif}\;x \leq 2 \cdot 10^{+14}:\\
\;\;\;\;\frac{-1 + -3 \cdot x}{\left(1 - x\right) \cdot \left(-1 - x\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{-3}{x}\\


\end{array}

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 3 regimes
  2. if x < -4e9

    1. Initial program 60.1

      \[\frac{x}{x + 1} - \frac{x + 1}{x - 1} \]
    2. Simplified60.1

      \[\leadsto \color{blue}{\frac{-1 - x}{x + -1} - \frac{x}{-1 - x}} \]
      Proof
      (-.f64 (/.f64 (-.f64 -1 x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (+.f64 x 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite=> metadata-eval -1))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite<= metadata-eval (/.f64 1 -1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (/.f64 1 (Rewrite<= metadata-eval (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)) 1))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 1) (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 x (+.f64 x 1))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite=> /-rgt-identity_binary64 (neg.f64 (/.f64 x (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (Rewrite=> remove-double-neg_binary64 (/.f64 x (+.f64 x 1))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 x (+.f64 x 1)) (/.f64 (+.f64 x 1) (-.f64 x 1)))): 31 points increase in error, 0 points decrease in error
    3. Taylor expanded in x around inf 0.3

      \[\leadsto \color{blue}{-\left(\frac{1}{{x}^{2}} + 3 \cdot \frac{1}{x}\right)} \]
    4. Simplified0.0

      \[\leadsto \color{blue}{\frac{-3}{x} - \frac{\frac{1}{x}}{x}} \]
      Proof
      (-.f64 (/.f64 -3 x) (/.f64 (/.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 3)) x) (/.f64 (/.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 3 x))) (/.f64 (/.f64 1 x) x)): 0 points increase in error, 11 points decrease in error
      (-.f64 (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 1)) x)) (/.f64 (/.f64 1 x) x)): 0 points increase in error, 7 points decrease in error
      (-.f64 (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 1 x)))) (/.f64 (/.f64 1 x) x)): 7 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 3 (/.f64 1 x)))) (/.f64 (/.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (-.f64 (-.f64 0 (*.f64 3 (/.f64 1 x))) (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 x x)))): 11 points increase in error, 0 points decrease in error
      (-.f64 (-.f64 0 (*.f64 3 (/.f64 1 x))) (/.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 x 2)))): 0 points increase in error, 11 points decrease in error
      (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 (*.f64 3 (/.f64 1 x)) (/.f64 1 (pow.f64 x 2))))): 0 points increase in error, 0 points decrease in error
      (-.f64 0 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x))))): 7 points increase in error, 0 points decrease in error
      (Rewrite<= neg-sub0_binary64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x))))): 11 points increase in error, 0 points decrease in error
    5. Applied egg-rr0.0

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

    if -4e9 < x < 2e14

    1. Initial program 0.5

      \[\frac{x}{x + 1} - \frac{x + 1}{x - 1} \]
    2. Simplified0.5

      \[\leadsto \color{blue}{\frac{-1 - x}{x + -1} - \frac{x}{-1 - x}} \]
      Proof
      (-.f64 (/.f64 (-.f64 -1 x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (+.f64 x 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite=> metadata-eval -1))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite<= metadata-eval (/.f64 1 -1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (/.f64 1 (Rewrite<= metadata-eval (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)) 1))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 1) (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 x (+.f64 x 1))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite=> /-rgt-identity_binary64 (neg.f64 (/.f64 x (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (Rewrite=> remove-double-neg_binary64 (/.f64 x (+.f64 x 1))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 x (+.f64 x 1)) (/.f64 (+.f64 x 1) (-.f64 x 1)))): 31 points increase in error, 0 points decrease in error
    3. Applied egg-rr0.5

      \[\leadsto \color{blue}{\frac{\left(x + 1\right) \cdot \left(-1 - x\right) - \left(1 - x\right) \cdot x}{\left(1 - x\right) \cdot \left(-1 - x\right)}} \]
    4. Taylor expanded in x around 0 0.0

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

    if 2e14 < x

    1. Initial program 60.4

      \[\frac{x}{x + 1} - \frac{x + 1}{x - 1} \]
    2. Simplified60.4

      \[\leadsto \color{blue}{\frac{-1 - x}{x + -1} - \frac{x}{-1 - x}} \]
      Proof
      (-.f64 (/.f64 (-.f64 -1 x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))) (+.f64 x -1)) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (/.f64 (neg.f64 (+.f64 x 1)) (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (/.f64 x (-.f64 -1 x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 -1 x))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) x))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 1) (neg.f64 x))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 x 1))))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 x (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (+.f64 x 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite=> metadata-eval -1))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (Rewrite<= metadata-eval (/.f64 1 -1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (/.f64 x (+.f64 x 1)) (/.f64 1 (Rewrite<= metadata-eval (neg.f64 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 x (+.f64 x 1)) (neg.f64 1)) 1))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 1) (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 x (+.f64 x 1))) 1)): 0 points increase in error, 31 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 x (+.f64 x 1)))) 1)): 0 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (neg.f64 1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (Rewrite=> /-rgt-identity_binary64 (neg.f64 (/.f64 x (+.f64 x 1))))): 31 points increase in error, 0 points decrease in error
      (-.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (-.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))) (neg.f64 (/.f64 x (+.f64 x 1)))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))) (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))))): 0 points increase in error, 31 points decrease in error
      (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (neg.f64 (/.f64 x (+.f64 x 1)))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1))))): 0 points increase in error, 0 points decrease in error
      (+.f64 (Rewrite=> remove-double-neg_binary64 (/.f64 x (+.f64 x 1))) (neg.f64 (/.f64 (+.f64 x 1) (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 x (+.f64 x 1)) (/.f64 (+.f64 x 1) (-.f64 x 1)))): 31 points increase in error, 0 points decrease in error
    3. Taylor expanded in x around inf 0.0

      \[\leadsto \color{blue}{\frac{-3}{x}} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification0.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4000000000:\\ \;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\ \mathbf{elif}\;x \leq 2 \cdot 10^{+14}:\\ \;\;\;\;\frac{-1 + -3 \cdot x}{\left(1 - x\right) \cdot \left(-1 - x\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-3}{x}\\ \end{array} \]

Alternatives

Alternative 1
Error0.0
Cost1344
\[\frac{-3}{1 - x} \cdot \frac{x}{-1 - x} + \frac{-1}{\left(1 - x\right) \cdot \left(-1 - x\right)} \]
Alternative 2
Error0.1
Cost1097
\[\begin{array}{l} \mathbf{if}\;x \leq -600000 \lor \neg \left(x \leq 390000\right):\\ \;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{1 + x} + \frac{-1 - x}{x + -1}\\ \end{array} \]
Alternative 3
Error0.7
Cost713
\[\begin{array}{l} \mathbf{if}\;x \leq -1 \lor \neg \left(x \leq 1\right):\\ \;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\ \mathbf{else}:\\ \;\;\;\;1 + x \cdot 3\\ \end{array} \]
Alternative 4
Error0.6
Cost713
\[\begin{array}{l} \mathbf{if}\;x \leq -1 \lor \neg \left(x \leq 1\right):\\ \;\;\;\;\frac{-3 + \frac{-1}{x}}{x}\\ \mathbf{else}:\\ \;\;\;\;1 + x \cdot \left(x + 3\right)\\ \end{array} \]
Alternative 5
Error1.0
Cost584
\[\begin{array}{l} \mathbf{if}\;x \leq -1:\\ \;\;\;\;\frac{-3}{x}\\ \mathbf{elif}\;x \leq 1:\\ \;\;\;\;1 + x \cdot 3\\ \mathbf{else}:\\ \;\;\;\;\frac{-3}{x}\\ \end{array} \]
Alternative 6
Error1.4
Cost456
\[\begin{array}{l} \mathbf{if}\;x \leq -1:\\ \;\;\;\;\frac{-3}{x}\\ \mathbf{elif}\;x \leq 1:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{-3}{x}\\ \end{array} \]
Alternative 7
Error31.6
Cost64
\[1 \]

Error

Reproduce

herbie shell --seed 2022340 
(FPCore (x)
  :name "Asymptote C"
  :precision binary64
  (- (/ x (+ x 1.0)) (/ (+ x 1.0) (- x 1.0))))