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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -4.2459051660554507 \cdot 10^{-35} \lor \neg \left(\varepsilon \le 2.083346019454022 \cdot 10^{-42}\right):\\ \;\;\;\;\frac{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} \cdot \frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} + \tan x}\\ \mathbf{else}:\\ \;\;\;\;\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot \frac{1}{3} + x\right) + \varepsilon\\ \end{array}\]

Original	37.1
Target	15.7
Herbie	13.4

Derivation

Split input into 2 regimes
if eps < -4.2459051660554507e-35 or 2.083346019454022e-42 < eps
1. Initial program 30.8
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Initial simplification30.8
  \[\leadsto \tan \left(\varepsilon + x\right) - \tan x\]
3. Using strategy rm
4. Applied tan-sum2.8
  \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
5. Using strategy rm
6. Applied flip--3.0
  \[\leadsto \color{blue}{\frac{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} \cdot \frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} + \tan x}}\]
if -4.2459051660554507e-35 < eps < 2.083346019454022e-42
1. Initial program 45.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Initial simplification45.4
  \[\leadsto \tan \left(\varepsilon + x\right) - \tan x\]
3. Taylor expanded around 0 27.2
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)}\]
4. Simplified27.2
  \[\leadsto \color{blue}{\varepsilon + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(x + \frac{1}{3} \cdot \varepsilon\right)}\]
Recombined 2 regimes into one program.
Final simplification13.4
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -4.2459051660554507 \cdot 10^{-35} \lor \neg \left(\varepsilon \le 2.083346019454022 \cdot 10^{-42}\right):\\ \;\;\;\;\frac{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} \cdot \frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} + \tan x}\\ \mathbf{else}:\\ \;\;\;\;\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot \frac{1}{3} + x\right) + \varepsilon\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -4.2459051660554507e-35 or 2.083346019454022e-42 < eps`

`if -4.2459051660554507e-35 < eps < 2.083346019454022e-42`

Runtime

In
Out