Initial program 33.5
\[\left|\left(\left(\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}\right) \bmod a\right)\right|\]
- Using strategy
rm Applied add-log-exp33.5
\[\leadsto \left|\left(\color{blue}{\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right)} \bmod a\right)\right|\]
- Using strategy
rm Applied add-cube-cbrt33.5
\[\leadsto \left|\color{blue}{\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}\right) \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}}\right|\]
- Using strategy
rm Applied add-cube-cbrt33.5
\[\leadsto \left|\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}\right) \cdot \sqrt[3]{\left(\left(\log \left(e^{\color{blue}{\left(\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}} \cdot \sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right) \cdot \sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}}}\right)\right) \bmod a\right)}\right|\]
Applied exp-prod33.5
\[\leadsto \left|\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}\right) \cdot \sqrt[3]{\left(\left(\log \color{blue}{\left({\left(e^{\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}} \cdot \sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}}\right)}^{\left(\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)}\right)}\right) \bmod a\right)}\right|\]
- Using strategy
rm Applied add-cube-cbrt33.5
\[\leadsto \left|\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\color{blue}{\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}\right) \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}}}\right) \cdot \sqrt[3]{\left(\left(\log \left({\left(e^{\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}} \cdot \sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}}\right)}^{\left(\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)}\right)\right) \bmod a\right)}\right|\]
Final simplification33.5
\[\leadsto \left|\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)} \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}\right) \cdot \sqrt[3]{\left(\left(\log \left(e^{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)\right) \bmod a\right)}}\right) \cdot \sqrt[3]{\left(\left(\log \left({\left(e^{\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}} \cdot \sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}}\right)}^{\left(\sqrt[3]{\tan^{-1}_* \frac{\mathsf{expm1}\left(\sin \left(\mathsf{expm1}\left(a\right)\right)\right)}{\tan^{-1} a}}\right)}\right)\right) \bmod a\right)}\right|\]