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

↓

\[\begin{array}{l} \mathbf{if}\;(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_* \le -3.1068469719484584 \cdot 10^{-28}:\\ \;\;\;\;\frac{(\left(\cos x\right) \cdot \left(\tan x + \tan \varepsilon\right) + \left((\left(\sin x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right) + \left(-\sin x\right))_*\right))_*}{(\left(\tan \varepsilon \cdot \cos x\right) \cdot \left(-\tan x\right) + \left(\cos x\right))_*}\\ \mathbf{if}\;(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_* \le 5.858083040047354 \cdot 10^{-17}:\\ \;\;\;\;(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;\frac{(\left(\cos x\right) \cdot \left(\tan x + \tan \varepsilon\right) + \left((\left(\sin x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right) + \left(-\sin x\right))_*\right))_*}{(\left(\tan \varepsilon \cdot \cos x\right) \cdot \left(-\tan x\right) + \left(\cos x\right))_*}\\ \end{array}\]

Original	37.1
Target	15.6
Herbie	13.7

Derivation

Split input into 2 regimes
if (fma (* x eps) (fma (* x eps) eps eps) eps) < -3.1068469719484584e-28 or 5.858083040047354e-17 < (fma (* x eps) (fma (* x eps) eps eps) eps)
1. Initial program 34.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum8.6
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied add-log-exp8.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
6. Using strategy rm
7. Applied tan-quot8.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)} - \color{blue}{\frac{\sin x}{\cos x}}\]
8. Applied frac-sub8.8
  \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) \cdot \sin x}{\left(1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) \cdot \cos x}}\]
9. Applied simplify8.7
  \[\leadsto \frac{\color{blue}{(\left(\cos x\right) \cdot \left(\tan x + \tan \varepsilon\right) + \left((\left(\sin x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right) + \left(-\sin x\right))_*\right))_*}}{\left(1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) \cdot \cos x}\]
10. Applied simplify8.6
  \[\leadsto \frac{(\left(\cos x\right) \cdot \left(\tan x + \tan \varepsilon\right) + \left((\left(\sin x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right) + \left(-\sin x\right))_*\right))_*}{\color{blue}{(\left(\tan \varepsilon \cdot \cos x\right) \cdot \left(-\tan x\right) + \left(\cos x\right))_*}}\]
if -3.1068469719484584e-28 < (fma (* x eps) (fma (* x eps) eps eps) eps) < 5.858083040047354e-17
1. Initial program 41.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 23.0
  \[\leadsto \color{blue}{\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)}\]
3. Applied simplify21.9
  \[\leadsto \color{blue}{(\left(x \cdot \varepsilon\right) \cdot \left((\left(x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon)_*\right) + \varepsilon)_*}\]
Recombined 2 regimes into one program.

Error

Target

Derivation

`if (fma (* x eps) (fma (* x eps) eps eps) eps) < -3.1068469719484584e-28 or 5.858083040047354e-17 < (fma (* x eps) (fma (* x eps) eps eps) eps)`

`if -3.1068469719484584e-28 < (fma (* x eps) (fma (* x eps) eps eps) eps) < 5.858083040047354e-17`

Runtime