Initial program 29.8
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum2.4
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
Simplified2.4
\[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
- Using strategy
rm Applied add-cube-cbrt2.7
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan \varepsilon \cdot \tan x} - \color{blue}{\left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}}\]
Applied flip--2.8
\[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{1 + \tan \varepsilon \cdot \tan x}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
Applied associate-/r/2.8
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} \cdot \left(1 + \tan \varepsilon \cdot \tan x\right)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
Applied prod-diff2.7
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}, 1 + \tan \varepsilon \cdot \tan x, -\sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right) + \mathsf{fma}\left(-\sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right)}\]
Simplified2.4
\[\leadsto \color{blue}{\left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right)} + \mathsf{fma}\left(-\sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right)\]
Simplified2.5
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right) + \color{blue}{\mathsf{fma}\left(-\tan x, 1, \tan x\right)}\]
- Using strategy
rm Applied add-sqr-sqrt2.5
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \color{blue}{\sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} \cdot \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied *-un-lft-identity2.5
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{\color{blue}{1 \cdot 1} - \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} \cdot \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied difference-of-squares2.5
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{\color{blue}{\left(1 + \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right) \cdot \left(1 - \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied *-commutative2.5
\[\leadsto \left(\frac{\color{blue}{\mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right) \cdot \left(\tan x + \tan \varepsilon\right)}}{\left(1 + \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right) \cdot \left(1 - \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right)} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied times-frac2.4
\[\leadsto \left(\color{blue}{\frac{\mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 + \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}} \cdot \frac{\tan x + \tan \varepsilon}{1 - \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied fma-neg2.4
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 + \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}}, \frac{\tan x + \tan \varepsilon}{1 - \sqrt{\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}}, -\tan x\right)} + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Initial program 30.6
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum3.9
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
Simplified3.9
\[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]
- Using strategy
rm Applied add-cube-cbrt4.2
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan \varepsilon \cdot \tan x} - \color{blue}{\left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}}\]
Applied flip--4.2
\[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{1 + \tan \varepsilon \cdot \tan x}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
Applied associate-/r/4.3
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} \cdot \left(1 + \tan \varepsilon \cdot \tan x\right)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
Applied prod-diff4.2
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}, 1 + \tan \varepsilon \cdot \tan x, -\sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right) + \mathsf{fma}\left(-\sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right)}\]
Simplified3.9
\[\leadsto \color{blue}{\left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right)} + \mathsf{fma}\left(-\sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}, \sqrt[3]{\tan x} \cdot \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right)\right)\]
Simplified4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right) + \color{blue}{\mathsf{fma}\left(-\tan x, 1, \tan x\right)}\]
- Using strategy
rm Applied add-cbrt-cube4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \color{blue}{\sqrt[3]{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied add-cbrt-cube4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\tan \varepsilon \cdot \color{blue}{\sqrt[3]{\left(\tan x \cdot \tan x\right) \cdot \tan x}}\right) \cdot \sqrt[3]{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied add-cbrt-cube4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \left(\color{blue}{\sqrt[3]{\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon}} \cdot \sqrt[3]{\left(\tan x \cdot \tan x\right) \cdot \tan x}\right) \cdot \sqrt[3]{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied cbrt-unprod4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \color{blue}{\sqrt[3]{\left(\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon\right) \cdot \left(\left(\tan x \cdot \tan x\right) \cdot \tan x\right)}} \cdot \sqrt[3]{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Applied cbrt-unprod4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \color{blue}{\sqrt[3]{\left(\left(\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon\right) \cdot \left(\left(\tan x \cdot \tan x\right) \cdot \tan x\right)\right) \cdot \left(\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right)}}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]
Simplified4.0
\[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot \mathsf{fma}\left(\tan \varepsilon, \tan x, 1\right)}{1 - \sqrt[3]{\color{blue}{{\left(\tan \varepsilon\right)}^{3} \cdot \left({\left(\tan x\right)}^{3} \cdot \left(\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)\right)\right)}}} - \tan x\right) + \mathsf{fma}\left(-\tan x, 1, \tan x\right)\]