Initial program 36.9
\[\sin \left(x + \varepsilon\right) - \sin x\]
- Using strategy
rm Applied sin-sum22.0
\[\leadsto \color{blue}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - \sin x\]
- Using strategy
rm Applied *-un-lft-identity22.0
\[\leadsto \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \color{blue}{1 \cdot \sin x}\]
Applied *-un-lft-identity22.0
\[\leadsto \color{blue}{1 \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - 1 \cdot \sin x\]
Applied distribute-lft-out--22.0
\[\leadsto \color{blue}{1 \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x\right)}\]
Simplified0.4
\[\leadsto 1 \cdot \color{blue}{\mathsf{fma}\left(\sin x, \cos \varepsilon - 1, \cos x \cdot \sin \varepsilon\right)}\]
- Using strategy
rm Applied add-cube-cbrt0.7
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \cos \varepsilon - 1, \color{blue}{\left(\left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \sqrt[3]{\cos x}\right)} \cdot \sin \varepsilon\right)\]
Applied associate-*l*0.7
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \cos \varepsilon - 1, \color{blue}{\left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)}\right)\]
- Using strategy
rm Applied add-log-exp0.7
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \cos \varepsilon - \color{blue}{\log \left(e^{1}\right)}, \left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)\right)\]
Applied add-log-exp0.8
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \color{blue}{\log \left(e^{\cos \varepsilon}\right)} - \log \left(e^{1}\right), \left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)\right)\]
Applied diff-log0.8
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \color{blue}{\log \left(\frac{e^{\cos \varepsilon}}{e^{1}}\right)}, \left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)\right)\]
Simplified0.8
\[\leadsto 1 \cdot \mathsf{fma}\left(\sin x, \log \color{blue}{\left(e^{\cos \varepsilon - 1}\right)}, \left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)\right)\]
Final simplification0.8
\[\leadsto \mathsf{fma}\left(\sin x, \log \left(e^{\cos \varepsilon - 1}\right), \left(\sqrt[3]{\cos x} \cdot \sqrt[3]{\cos x}\right) \cdot \left(\sqrt[3]{\cos x} \cdot \sin \varepsilon\right)\right)\]