\(\log_* (1 + (e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \left(\sin x \cdot \left(\cos \varepsilon - 1\right)\right))_*} - 1)^*)\)
- Started with
\[\sin \left(x + \varepsilon\right) - \sin x\]
36.5
- Using strategy
rm 36.5
- Applied sin-sum to get
\[\color{red}{\sin \left(x + \varepsilon\right)} - \sin x \leadsto \color{blue}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - \sin x\]
21.7
- Using strategy
rm 21.7
- Applied log1p-expm1-u to get
\[\color{red}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x} \leadsto \color{blue}{\log_* (1 + (e^{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x} - 1)^*)}\]
21.8
- Applied simplify to get
\[\log_* (1 + \color{red}{(e^{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x} - 1)^*}) \leadsto \log_* (1 + \color{blue}{(e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \left(\cos \varepsilon \cdot \sin x - \sin x\right))_*} - 1)^*})\]
0.5
- Using strategy
rm 0.5
- Applied *-un-lft-identity to get
\[\log_* (1 + (e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \left(\cos \varepsilon \cdot \sin x - \color{red}{\sin x}\right))_*} - 1)^*) \leadsto \log_* (1 + (e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \left(\cos \varepsilon \cdot \sin x - \color{blue}{1 \cdot \sin x}\right))_*} - 1)^*)\]
0.5
- Applied distribute-rgt-out-- to get
\[\log_* (1 + (e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \color{red}{\left(\cos \varepsilon \cdot \sin x - 1 \cdot \sin x\right)})_*} - 1)^*) \leadsto \log_* (1 + (e^{(\left(\sin \varepsilon\right) * \left(\cos x\right) + \color{blue}{\left(\sin x \cdot \left(\cos \varepsilon - 1\right)\right)})_*} - 1)^*)\]
0.5
