- Split input into 2 regimes
if (/ (/ (cos (* x 2)) (* (* sin x) cos)) (* (* sin x) cos)) < 1.6473990936411884e+308
Initial program 26.3
\[\frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot {sin}^{2}\right) \cdot x\right)}\]
- Using strategy
rm Applied unpow226.3
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot \color{blue}{\left(sin \cdot sin\right)}\right) \cdot x\right)}\]
Applied associate-*r*20.2
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\color{blue}{\left(\left(x \cdot sin\right) \cdot sin\right)} \cdot x\right)}\]
- Using strategy
rm Applied add-exp-log21.3
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{e^{\log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}}\]
Applied add-exp-log35.7
\[\leadsto \frac{\color{blue}{e^{\log \left(\cos \left(2 \cdot x\right)\right)}}}{e^{\log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}\]
Applied div-exp35.7
\[\leadsto \color{blue}{e^{\log \left(\cos \left(2 \cdot x\right)\right) - \log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}\]
Simplified11.6
\[\leadsto e^{\color{blue}{\log \left(\frac{\cos \left(x \cdot 2\right)}{\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)}\right)}}\]
- Using strategy
rm Applied rem-exp-log1.9
\[\leadsto \color{blue}{\frac{\cos \left(x \cdot 2\right)}{\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)}}\]
- Using strategy
rm Applied associate-/r*1.6
\[\leadsto \color{blue}{\frac{\frac{\cos \left(x \cdot 2\right)}{\left(sin \cdot x\right) \cdot cos}}{\left(sin \cdot x\right) \cdot cos}}\]
if 1.6473990936411884e+308 < (/ (/ (cos (* x 2)) (* (* sin x) cos)) (* (* sin x) cos))
Initial program 60.0
\[\frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot {sin}^{2}\right) \cdot x\right)}\]
- Using strategy
rm Applied unpow260.0
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot \color{blue}{\left(sin \cdot sin\right)}\right) \cdot x\right)}\]
Applied associate-*r*60.0
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\color{blue}{\left(\left(x \cdot sin\right) \cdot sin\right)} \cdot x\right)}\]
- Using strategy
rm Applied add-exp-log60.0
\[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{e^{\log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}}\]
Applied add-exp-log60.0
\[\leadsto \frac{\color{blue}{e^{\log \left(\cos \left(2 \cdot x\right)\right)}}}{e^{\log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}\]
Applied div-exp60.0
\[\leadsto \color{blue}{e^{\log \left(\cos \left(2 \cdot x\right)\right) - \log \left({cos}^{2} \cdot \left(\left(\left(x \cdot sin\right) \cdot sin\right) \cdot x\right)\right)}}\]
Simplified60.0
\[\leadsto e^{\color{blue}{\log \left(\frac{\cos \left(x \cdot 2\right)}{\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)}\right)}}\]
- Using strategy
rm Applied rem-exp-log60.0
\[\leadsto \color{blue}{\frac{\cos \left(x \cdot 2\right)}{\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)}}\]
- Using strategy
rm Applied add-exp-log60.0
\[\leadsto \frac{\cos \left(x \cdot 2\right)}{\color{blue}{e^{\log \left(\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)\right)}}}\]
Applied add-exp-log60.0
\[\leadsto \frac{\color{blue}{e^{\log \left(\cos \left(x \cdot 2\right)\right)}}}{e^{\log \left(\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)\right)}}\]
Applied div-exp60.0
\[\leadsto \color{blue}{e^{\log \left(\cos \left(x \cdot 2\right)\right) - \log \left(\left(\left(sin \cdot x\right) \cdot cos\right) \cdot \left(\left(sin \cdot x\right) \cdot cos\right)\right)}}\]
Simplified7.5
\[\leadsto e^{\color{blue}{\log \left(\frac{\cos \left(2 \cdot x\right)}{\left(sin \cdot \left(cos \cdot x\right)\right) \cdot \left(sin \cdot \left(cos \cdot x\right)\right)}\right)}}\]
- Recombined 2 regimes into one program.
Final simplification1.7
\[\leadsto \begin{array}{l}
\mathbf{if}\;\frac{\frac{\cos \left(2 \cdot x\right)}{cos \cdot \left(x \cdot sin\right)}}{cos \cdot \left(x \cdot sin\right)} \le 1.6473990936411884 \cdot 10^{+308}:\\
\;\;\;\;\frac{\frac{\cos \left(2 \cdot x\right)}{cos \cdot \left(x \cdot sin\right)}}{cos \cdot \left(x \cdot sin\right)}\\
\mathbf{else}:\\
\;\;\;\;e^{\log \left(\frac{\cos \left(2 \cdot x\right)}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\right)}\\
\end{array}\]