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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right) \le -7.890812128872918 \cdot 10^{-33}:\\ \;\;\;\;\frac{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} \cdot \frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} \cdot \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \cos x - \left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \sin x}{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \cos x}\\ \mathbf{if}\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right) \le 7.959372175528218 \cdot 10^{-27}:\\ \;\;\;\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) - \frac{\sin x}{\cos x}\\ \end{array}\]

Original	36.8
Target	15.0
Herbie	14.2

Derivation

Split input into 3 regimes
if (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < -7.890812128872918e-33
1. Initial program 34.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum10.2
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around inf 10.4
  \[\leadsto \color{blue}{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) - \frac{\sin x}{\cos x}}\]
5. Using strategy rm
6. Applied flip-+10.5
  \[\leadsto \color{blue}{\frac{\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} \cdot \frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} \cdot \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}}{\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}}} - \frac{\sin x}{\cos x}\]
7. Applied frac-sub10.4
  \[\leadsto \color{blue}{\frac{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} \cdot \frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} \cdot \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \cos x - \left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \sin x}{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) \cdot \cos x}}\]
if -7.890812128872918e-33 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < 7.959372175528218e-27
1. Initial program 40.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 16.5
  \[\leadsto \color{blue}{\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)}\]
if 7.959372175528218e-27 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x)))
1. Initial program 35.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum14.1
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around inf 14.3
  \[\leadsto \color{blue}{\left(\frac{\sin x}{\left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right) \cdot \cos x} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}\right) - \frac{\sin x}{\cos x}}\]
Recombined 3 regimes into one program.

Error

Target

Derivation

`if (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < -7.890812128872918e-33`

`if -7.890812128872918e-33 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < 7.959372175528218e-27`

`if 7.959372175528218e-27 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x)))`

Runtime