# ?

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)}


# Try it out?

Results

 In Out
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)}$ $\tan^{-1}_* \frac{\color{blue}{\left(x - x\right) + 1}}{1 + \left(x + x \cdot x\right)}$ $\tan^{-1}_* \frac{\color{blue}{0} + 1}{1 + \left(x + x \cdot x\right)}$ $\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}$

# 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)))