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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.8174464320865843 \cdot 10^{-17}:\\ \;\;\;\;(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan \varepsilon \cdot \tan x\right)}^{3}}\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x + \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) + 1\right) + \left(-\tan x\right))_*\\ \mathbf{if}\;\varepsilon \le 1.7836972326109573 \cdot 10^{-17}:\\ \;\;\;\;(\left(\varepsilon \cdot \varepsilon\right) \cdot \left((x \cdot \left(x \cdot \varepsilon\right) + x)_*\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan \varepsilon \cdot \tan x\right)}^{3}}\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x + \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) + 1\right) + \left(-\tan x\right))_*\\ \end{array}\]

Original	37.5
Target	15.4
Herbie	13.8

Derivation

Split input into 2 regimes
if eps < -1.8174464320865843e-17 or 1.7836972326109573e-17 < eps
1. Initial program 30.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum1.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3--1.1
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]
6. Applied associate-/r/1.1
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]
7. Applied fma-neg1.1
  \[\leadsto \color{blue}{(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\right) \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) + \left(-\tan x\right))_*}\]
if -1.8174464320865843e-17 < eps < 1.7836972326109573e-17
1. Initial program 45.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 29.4
  \[\leadsto \color{blue}{\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)}\]
3. Applied simplify28.2
  \[\leadsto \color{blue}{(\left(\varepsilon \cdot \varepsilon\right) \cdot \left((x \cdot \left(x \cdot \varepsilon\right) + x)_*\right) + \varepsilon)_*}\]
Recombined 2 regimes into one program.
Applied simplify13.8
\[\leadsto \color{blue}{\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.8174464320865843 \cdot 10^{-17}:\\ \;\;\;\;(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan \varepsilon \cdot \tan x\right)}^{3}}\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x + \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) + 1\right) + \left(-\tan x\right))_*\\ \mathbf{if}\;\varepsilon \le 1.7836972326109573 \cdot 10^{-17}:\\ \;\;\;\;(\left(\varepsilon \cdot \varepsilon\right) \cdot \left((x \cdot \left(x \cdot \varepsilon\right) + x)_*\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan \varepsilon \cdot \tan x\right)}^{3}}\right) \cdot \left(\left(\tan \varepsilon \cdot \tan x + \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) + 1\right) + \left(-\tan x\right))_*\\ \end{array}}\]

Error

Target

Derivation

`if eps < -1.8174464320865843e-17 or 1.7836972326109573e-17 < eps`

`if -1.8174464320865843e-17 < eps < 1.7836972326109573e-17`

Runtime