?

Average Error: 0.1 → 0.0
Time: 6.4s
Precision: binary64
Cost: 6912

?

\[-1000 \leq x \land x \leq 1000\]
\[\tan^{-1} \left(x + 1\right) - \tan^{-1} x \]
\[\tan^{-1}_* \frac{1}{1 + \left(x + x \cdot x\right)} \]
(FPCore (x) :precision binary64 (- (atan (+ x 1.0)) (atan x)))
(FPCore (x) :precision binary64 (atan2 1.0 (+ 1.0 (+ x (* x x)))))
double code(double x) {
	return atan((x + 1.0)) - atan(x);
}
double code(double x) {
	return atan2(1.0, (1.0 + (x + (x * x))));
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = atan((x + 1.0d0)) - atan(x)
end function
real(8) function code(x)
    real(8), intent (in) :: x
    code = atan2(1.0d0, (1.0d0 + (x + (x * x))))
end function
public static double code(double x) {
	return Math.atan((x + 1.0)) - Math.atan(x);
}
public static double code(double x) {
	return Math.atan2(1.0, (1.0 + (x + (x * x))));
}
def code(x):
	return math.atan((x + 1.0)) - math.atan(x)
def code(x):
	return math.atan2(1.0, (1.0 + (x + (x * x))))
function code(x)
	return Float64(atan(Float64(x + 1.0)) - atan(x))
end
function code(x)
	return atan(1.0, Float64(1.0 + Float64(x + Float64(x * x))))
end
function tmp = code(x)
	tmp = atan((x + 1.0)) - atan(x);
end
function tmp = code(x)
	tmp = atan2(1.0, (1.0 + (x + (x * x))));
end
code[x_] := N[(N[ArcTan[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[ArcTan[x], $MachinePrecision]), $MachinePrecision]
code[x_] := N[ArcTan[1.0 / N[(1.0 + N[(x + N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\tan^{-1} \left(x + 1\right) - \tan^{-1} x
\tan^{-1}_* \frac{1}{1 + \left(x + x \cdot x\right)}

Error?

Try it out?

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation?

  1. Initial program 0.1

    \[\tan^{-1} \left(x + 1\right) - \tan^{-1} x \]
  2. Applied egg-rr1.0

    \[\leadsto \color{blue}{\log \left(e^{\tan^{-1} \left(x + 1\right) - \tan^{-1} x}\right)} \]
  3. Applied egg-rr0.0

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

    \[\leadsto \color{blue}{\tan^{-1}_* \frac{1}{1 + \left(x + x \cdot x\right)}} \]
    Proof

    [Start]0.0

    \[ \tan^{-1}_* \frac{1 + \left(x - x\right)}{1 + \left(x + x \cdot x\right)} \]

    +-commutative [=>]0.0

    \[ \tan^{-1}_* \frac{\color{blue}{\left(x - x\right) + 1}}{1 + \left(x + x \cdot x\right)} \]

    +-inverses [=>]0.0

    \[ \tan^{-1}_* \frac{\color{blue}{0} + 1}{1 + \left(x + x \cdot x\right)} \]

    metadata-eval [=>]0.0

    \[ \tan^{-1}_* \frac{\color{blue}{1}}{1 + \left(x + x \cdot x\right)} \]
  5. Final simplification0.0

    \[\leadsto \tan^{-1}_* \frac{1}{1 + \left(x + x \cdot x\right)} \]

Alternatives

Alternative 1
Error1.8
Cost6784
\[\tan^{-1}_* \frac{x + \left(1 - x\right)}{1} \]

Error

Reproduce?

herbie shell --seed 1 
(FPCore (x)
  :name "atan(x+1) - atan(x)"
  :precision binary64
  :pre (and (<= -1000.0 x) (<= x 1000.0))
  (- (atan (+ x 1.0)) (atan x)))