Initial program 13.2
\[x + \left(\tan \left(y + z\right) - \tan a\right)\]
- Using strategy
rm Applied tan-sum0.2
\[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} - \tan a\right)\]
- Using strategy
rm Applied *-un-lft-identity0.2
\[\leadsto x + \left(\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} - \color{blue}{1 \cdot \tan a}\right)\]
Applied flip3--0.2
\[\leadsto x + \left(\frac{\tan y + \tan z}{\color{blue}{\frac{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}{1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)}}} - 1 \cdot \tan a\right)\]
Applied associate-/r/0.2
\[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right)\right)} - 1 \cdot \tan a\right)\]
Applied prod-diff0.2
\[\leadsto x + \color{blue}{\left(\mathsf{fma}\left(\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}, 1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right), -\tan a \cdot 1\right) + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)\right)}\]
Applied associate-+r+0.2
\[\leadsto \color{blue}{\left(x + \mathsf{fma}\left(\frac{\tan y + \tan z}{{1}^{3} - {\left(\tan y \cdot \tan z\right)}^{3}}, 1 \cdot 1 + \left(\left(\tan y \cdot \tan z\right) \cdot \left(\tan y \cdot \tan z\right) + 1 \cdot \left(\tan y \cdot \tan z\right)\right), -\tan a \cdot 1\right)\right) + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)}\]
Simplified0.3
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan y + \tan z}{1 - {\left(\tan y \cdot \tan z\right)}^{3}}, \mathsf{fma}\left(\mathsf{fma}\left(\tan y, \tan z, 1\right), \tan y \cdot \tan z, 1\right), \left(-\tan a\right) + x\right)} + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)\]
- Using strategy
rm Applied add-cbrt-cube0.3
\[\leadsto \mathsf{fma}\left(\frac{\tan y + \tan z}{1 - \color{blue}{\sqrt[3]{\left({\left(\tan y \cdot \tan z\right)}^{3} \cdot {\left(\tan y \cdot \tan z\right)}^{3}\right) \cdot {\left(\tan y \cdot \tan z\right)}^{3}}}}, \mathsf{fma}\left(\mathsf{fma}\left(\tan y, \tan z, 1\right), \tan y \cdot \tan z, 1\right), \left(-\tan a\right) + x\right) + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)\]
Simplified0.3
\[\leadsto \mathsf{fma}\left(\frac{\tan y + \tan z}{1 - \sqrt[3]{\color{blue}{{\left({\left(\tan y \cdot \tan z\right)}^{3}\right)}^{3}}}}, \mathsf{fma}\left(\mathsf{fma}\left(\tan y, \tan z, 1\right), \tan y \cdot \tan z, 1\right), \left(-\tan a\right) + x\right) + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)\]
Final simplification0.3
\[\leadsto \mathsf{fma}\left(\frac{\tan y + \tan z}{1 - \sqrt[3]{{\left({\left(\tan y \cdot \tan z\right)}^{3}\right)}^{3}}}, \mathsf{fma}\left(\mathsf{fma}\left(\tan y, \tan z, 1\right), \tan y \cdot \tan z, 1\right), \left(-\tan a\right) + x\right) + \mathsf{fma}\left(-\tan a, 1, \tan a \cdot 1\right)\]