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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.0971498034386314 \cdot 10^{-22}:\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 3.432974870891229 \cdot 10^{-42}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) + \left(-\tan x\right))_*\\ \end{array}\]

Original	37.2
Target	15.0
Herbie	15.5

Derivation

Split input into 2 regimes
if eps < -3.0971498034386314e-22 or 3.432974870891229e-42 < eps
1. Initial program 30.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--2.4
  \[\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/2.4
  \[\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-neg2.4
  \[\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. Using strategy rm
9. Applied swap-sqr2.4
  \[\leadsto (\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \color{blue}{\left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}}\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) + \left(-\tan x\right))_*\]
if -3.0971498034386314e-22 < eps < 3.432974870891229e-42
1. Initial program 45.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum45.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around 0 31.3
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
5. Simplified31.2
  \[\leadsto \color{blue}{(\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon)_*}\]
Recombined 2 regimes into one program.
Final simplification15.5
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.0971498034386314 \cdot 10^{-22}:\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 3.432974870891229 \cdot 10^{-42}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}\right) \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) + \left(-\tan x\right))_*\\ \end{array}\]

Error

Target

Derivation

`if eps < -3.0971498034386314e-22 or 3.432974870891229e-42 < eps`

`if -3.0971498034386314e-22 < eps < 3.432974870891229e-42`

Reproduce