Initial program 60.3
\[\cos^{-1} \left({\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
- Using strategy
rm Applied add-log-exp59.4
\[\leadsto \cos^{-1} \left({\color{blue}{\left(\log \left(e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}\right)\right)}}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt59.4
\[\leadsto \cos^{-1} \left({\left(\log \left(e^{\color{blue}{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied exp-prod59.4
\[\leadsto \cos^{-1} \left({\left(\log \color{blue}{\left({\left(e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)}^{\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}\right)}\right)}\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-pow59.1
\[\leadsto \cos^{-1} \left({\color{blue}{\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \log \left(e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt59.1
\[\leadsto \cos^{-1} \left({\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \log \color{blue}{\left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}} \cdot \sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)}\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-prod59.1
\[\leadsto \cos^{-1} \left({\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \color{blue}{\left(\log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)\right)}\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt59.1
\[\leadsto \cos^{-1} \left({\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \left(\log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \log \left(\sqrt{\color{blue}{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}} \cdot \sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}}\right)\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied sqrt-prod59.1
\[\leadsto \cos^{-1} \left({\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \left(\log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \log \color{blue}{\left(\sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}} \cdot \sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right)}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-prod59.1
\[\leadsto \cos^{-1} \left({\left(\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)} \cdot \left(\log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \color{blue}{\left(\log \left(\sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right) + \log \left(\sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right)\right)}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Final simplification59.1
\[\leadsto \cos^{-1} \left({\left(\left(\log \left(\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \left(\log \left(\sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right) + \log \left(\sqrt{\sqrt{e^{\sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right)\right)\right) \cdot \sqrt{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]