Initial program 30.2
\[\frac{1 - \cos x}{x \cdot x}\]
- Using strategy
rm Applied flip--30.3
\[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x}\]
Applied associate-/l/30.3
\[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}}\]
Simplified15.0
\[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}\]
- Using strategy
rm Applied add-sqr-sqrt38.8
\[\leadsto \frac{\sin x \cdot \sin x}{\left(x \cdot \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}\right) \cdot \left(1 + \cos x\right)}\]
Applied add-sqr-sqrt38.9
\[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right) \cdot \left(1 + \cos x\right)}\]
Applied swap-sqr38.9
\[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\sqrt{x} \cdot \sqrt{x}\right)\right)} \cdot \left(1 + \cos x\right)}\]
Applied associate-*l*39.0
\[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 + \cos x\right)\right)}}\]
Applied *-un-lft-identity39.0
\[\leadsto \frac{\sin x \cdot \color{blue}{\left(1 \cdot \sin x\right)}}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 + \cos x\right)\right)}\]
Applied associate-*r*39.0
\[\leadsto \frac{\color{blue}{\left(\sin x \cdot 1\right) \cdot \sin x}}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 + \cos x\right)\right)}\]
Applied times-frac31.6
\[\leadsto \color{blue}{\frac{\sin x \cdot 1}{\sqrt{x} \cdot \sqrt{x}} \cdot \frac{\sin x}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 + \cos x\right)}}\]
Simplified31.5
\[\leadsto \color{blue}{\frac{\sin x}{x}} \cdot \frac{\sin x}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 + \cos x\right)}\]
Simplified0.1
\[\leadsto \frac{\sin x}{x} \cdot \color{blue}{\frac{\tan \left(\frac{x}{2}\right)}{x}}\]
Taylor expanded around -inf 15.0
\[\leadsto \color{blue}{\frac{\sin x \cdot \sin \left(\frac{1}{2} \cdot x\right)}{\cos \left(\frac{1}{2} \cdot x\right) \cdot {x}^{2}}}\]
Simplified0.1
\[\leadsto \color{blue}{\frac{\frac{\sin \left(x \cdot \frac{1}{2}\right)}{x}}{\frac{\cos \left(x \cdot \frac{1}{2}\right)}{\frac{\sin x}{x}}}}\]
Final simplification0.1
\[\leadsto \frac{\frac{\sin \left(x \cdot \frac{1}{2}\right)}{x}}{\frac{\cos \left(x \cdot \frac{1}{2}\right)}{\frac{\sin x}{x}}}\]
