Initial program 61.0
\[\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-exp60.1
\[\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-sqrt60.1
\[\leadsto \cos^{-1} \left({\left(\log \color{blue}{\left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}} \cdot \sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)}\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-prod60.1
\[\leadsto \cos^{-1} \left({\color{blue}{\left(\log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right) + \log \left(\sqrt{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-sqrt60.1
\[\leadsto \cos^{-1} \left({\left(\log \left(\sqrt{\color{blue}{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}} \cdot \sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}}\right) + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied sqrt-prod60.2
\[\leadsto \cos^{-1} \left({\left(\log \color{blue}{\left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}} \cdot \sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)} + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-prod60.2
\[\leadsto \cos^{-1} \left({\left(\color{blue}{\left(\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right) + \log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)\right)} + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Simplified60.2
\[\leadsto \cos^{-1} \left({\left(\left(\color{blue}{\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right)} + \log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}}\right)\right) + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Simplified60.2
\[\leadsto \cos^{-1} \left({\left(\left(\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right) + \color{blue}{\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right)}\right) + \log \left(\sqrt{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 pow160.2
\[\leadsto \cos^{-1} \left({\left(\left(\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right) + \log \left(\sqrt{\color{blue}{{\left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}\right)}^{1}}}\right)\right) + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied sqrt-pow160.2
\[\leadsto \cos^{-1} \left({\left(\left(\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right) + \log \color{blue}{\left({\left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}\right)}^{\left(\frac{1}{2}\right)}\right)}\right) + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Applied log-pow60.1
\[\leadsto \cos^{-1} \left({\left(\left(\log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right) + \color{blue}{\frac{1}{2} \cdot \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}\right)}\right) + \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]
Final simplification60.1
\[\leadsto \cos^{-1} \left({\left(\log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left(a \cdot a\right)\right)}}\right) + \left(\frac{1}{2} \cdot \log \left(\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}\right) + \log \left(\sqrt{\sqrt{e^{\left(\left(\cosh a\right) \bmod \left({a}^{2}\right)\right)}}}\right)\right)\right)}^{\left(\mathsf{log1p}\left(a\right)\right)}\right)\]