Average Error: 15.3 → 15.3
Time: 25.3s
Precision: 64
Internal Precision: 1344
${\left(\tan^{-1} x\right)}^{2} - {\left(\tan^{-1} \left(x + 1\right)\right)}^{2}$
$\frac{\sqrt[3]{{\left({\left(\tan^{-1} x\right)}^{3}\right)}^{\left(3 + 1\right)}} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right) + \tan^{-1} x \cdot \tan^{-1} x}$

# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 15.3

${\left(\tan^{-1} x\right)}^{2} - {\left(\tan^{-1} \left(x + 1\right)\right)}^{2}$
2. Initial simplification15.3

$\leadsto \tan^{-1} x \cdot \tan^{-1} x - \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)$
3. Using strategy rm
4. Applied flip--15.3

$\leadsto \color{blue}{\frac{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \left(\tan^{-1} x \cdot \tan^{-1} x\right) - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}}$
5. Using strategy rm

$\leadsto \frac{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \left(\tan^{-1} x \cdot \color{blue}{\sqrt[3]{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x}}\right) - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$

$\leadsto \frac{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \left(\color{blue}{\sqrt[3]{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x}} \cdot \sqrt[3]{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x}\right) - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$
8. Applied cbrt-unprod30.5

$\leadsto \frac{\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \color{blue}{\sqrt[3]{\left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right) \cdot \left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right)}} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$

$\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \left(\tan^{-1} x \cdot \tan^{-1} x\right)\right) \cdot \left(\tan^{-1} x \cdot \tan^{-1} x\right)}} \cdot \sqrt[3]{\left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right) \cdot \left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right)} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$
10. Applied cbrt-unprod15.3

$\leadsto \frac{\color{blue}{\sqrt[3]{\left(\left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \left(\tan^{-1} x \cdot \tan^{-1} x\right)\right) \cdot \left(\tan^{-1} x \cdot \tan^{-1} x\right)\right) \cdot \left(\left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right) \cdot \left(\left(\tan^{-1} x \cdot \tan^{-1} x\right) \cdot \tan^{-1} x\right)\right)}} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$
11. Simplified15.3

$\leadsto \frac{\sqrt[3]{\color{blue}{{\left({\left(\tan^{-1} x\right)}^{3}\right)}^{\left(3 + 1\right)}}} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} x \cdot \tan^{-1} x + \tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)}$
12. Final simplification15.3

$\leadsto \frac{\sqrt[3]{{\left({\left(\tan^{-1} x\right)}^{3}\right)}^{\left(3 + 1\right)}} - \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right) \cdot \left(\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right)\right)}{\tan^{-1} \left(x + 1\right) \cdot \tan^{-1} \left(x + 1\right) + \tan^{-1} x \cdot \tan^{-1} x}$

# Runtime

Time bar (total: 25.3s)Debug log

herbie shell --seed '#(2775764126 3555076145 3898259844 1891440260 2599947619 1948460636)'
(FPCore (x)
:name "atan(x)^2-atan(x+1)^2"
(- (pow (atan x) 2) (pow (atan (+ x 1)) 2)))