Initial program 30.6
\[\frac{1 - \cos x}{x \cdot x}\]
Initial simplification30.6
\[\leadsto \frac{1 - \cos x}{x \cdot x}\]
- Using strategy
rm Applied flip--30.7
\[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x}\]
Applied associate-/l/30.7
\[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}}\]
Simplified15.2
\[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}\]
Taylor expanded around inf 15.2
\[\leadsto \color{blue}{\frac{{\left(\sin x\right)}^{2}}{{x}^{2} \cdot \left(\cos x + 1\right)}}\]
Simplified15.3
\[\leadsto \color{blue}{\frac{\tan \left(\frac{x}{2}\right)}{\frac{x \cdot x}{\sin x}}}\]
- Using strategy
rm Applied *-un-lft-identity15.3
\[\leadsto \frac{\tan \left(\frac{x}{2}\right)}{\frac{x \cdot x}{\color{blue}{1 \cdot \sin x}}}\]
Applied times-frac0.4
\[\leadsto \frac{\tan \left(\frac{x}{2}\right)}{\color{blue}{\frac{x}{1} \cdot \frac{x}{\sin x}}}\]
Applied *-un-lft-identity0.4
\[\leadsto \frac{\color{blue}{1 \cdot \tan \left(\frac{x}{2}\right)}}{\frac{x}{1} \cdot \frac{x}{\sin x}}\]
Applied times-frac0.2
\[\leadsto \color{blue}{\frac{1}{\frac{x}{1}} \cdot \frac{\tan \left(\frac{x}{2}\right)}{\frac{x}{\sin x}}}\]
Simplified0.2
\[\leadsto \color{blue}{\frac{1}{x}} \cdot \frac{\tan \left(\frac{x}{2}\right)}{\frac{x}{\sin x}}\]
- Using strategy
rm Applied associate-*l/0.1
\[\leadsto \color{blue}{\frac{1 \cdot \frac{\tan \left(\frac{x}{2}\right)}{\frac{x}{\sin x}}}{x}}\]
Simplified0.1
\[\leadsto \frac{\color{blue}{\frac{\sin x}{x} \cdot \tan \left(\frac{x}{2}\right)}}{x}\]
Final simplification0.1
\[\leadsto \frac{\frac{\sin x}{x} \cdot \tan \left(\frac{x}{2}\right)}{x}\]
