\(1 \cdot (\left(\cos x\right) * \left(\sin \varepsilon\right) + \left(\cos \varepsilon \cdot \sin x - \sin x\right))_*\)
- Started with
\[\sin \left(x + \varepsilon\right) - \sin x\]
36.6
- Using strategy
rm 36.6
- 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.9
- Using strategy
rm 21.9
- Applied *-un-lft-identity to get
\[\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \color{red}{\sin x} \leadsto \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \color{blue}{1 \cdot \sin x}\]
21.9
- Applied *-un-lft-identity to get
\[\color{red}{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - 1 \cdot \sin x \leadsto \color{blue}{1 \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)} - 1 \cdot \sin x\]
21.9
- Applied distribute-lft-out-- to get
\[\color{red}{1 \cdot \left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - 1 \cdot \sin x} \leadsto \color{blue}{1 \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x\right)}\]
21.9
- Applied simplify to get
\[1 \cdot \color{red}{\left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) - \sin x\right)} \leadsto 1 \cdot \color{blue}{(\left(\cos x\right) * \left(\sin \varepsilon\right) + \left(\cos \varepsilon \cdot \sin x - \sin x\right))_*}\]
0.4
- Removed slow pow expressions