\[\tan \left(x + \varepsilon\right) - \tan x\]

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.780037414592675 \cdot 10^{-63}:\\ \;\;\;\;\frac{\left(\tan \varepsilon + \tan x\right) \cdot (\left(\tan \varepsilon\right) \cdot \left(\tan x\right) + 1)_*}{(\left(\tan x \cdot \left(-\tan \varepsilon\right)\right) \cdot \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) + 1)_*} - \tan x\\ \mathbf{if}\;\varepsilon \le 2.055260594916271 \cdot 10^{-37}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \end{array}\]

Original	36.9
Target	15.3
Herbie	14.1

Derivation

Split input into 3 regimes
if eps < -3.780037414592675e-63
1. Initial program 29.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum4.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--4.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 + \tan x \cdot \tan \varepsilon}}} - \tan x\]
6. Applied associate-/r/4.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)} - \tan x\]
7. Applied fma-neg4.7
  \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) + \left(-\tan x\right))_*}\]
8. Taylor expanded around inf 4.7
  \[\leadsto (\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \color{blue}{\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}}}\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) + \left(-\tan x\right))_*\]
9. Applied simplify4.8
  \[\leadsto \color{blue}{\frac{\left(\tan \varepsilon + \tan x\right) \cdot (\left(\tan \varepsilon\right) \cdot \left(\tan x\right) + 1)_*}{(\left(\tan x \cdot \left(-\tan \varepsilon\right)\right) \cdot \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) + 1)_*} - \tan x}\]
if -3.780037414592675e-63 < eps < 2.055260594916271e-37
1. Initial program 46.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 29.8
  \[\leadsto \color{blue}{\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)}\]
3. Applied simplify28.6
  \[\leadsto \color{blue}{(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_*}\]
if 2.055260594916271e-37 < eps
1. Initial program 30.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum3.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--3.1
  \[\leadsto \color{blue}{\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}}\]
Recombined 3 regimes into one program.

Error

Target

Derivation

`if eps < -3.780037414592675e-63`

`if -3.780037414592675e-63 < eps < 2.055260594916271e-37`

`if 2.055260594916271e-37 < eps`

Runtime