Initial program 31.8
\[\frac{1 - \cos x}{x \cdot x}
\]
Applied egg-rr16.8
\[\leadsto \frac{\color{blue}{\left(\sin x \cdot \sin x\right) \cdot \frac{1}{1 + \cos x}}}{x \cdot x}
\]
Simplified16.6
\[\leadsto \frac{\color{blue}{\sin x \cdot \tan \left(\frac{x}{2}\right)}}{x \cdot x}
\]
Proof
(/.f64 (*.f64 (sin.f64 x) (tan.f64 (/.f64 x 2))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sin.f64 x) (Rewrite<= hang-0p-tan_binary64 (/.f64 (sin.f64 x) (+.f64 1 (cos.f64 x))))) (*.f64 x x)): 0 points increase in error, 5 points decrease in error
(/.f64 (*.f64 (sin.f64 x) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (sin.f64 x) 1)) (+.f64 1 (cos.f64 x)))) (*.f64 x x)): 5 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sin.f64 x) (Rewrite<= associate-*r/_binary64 (*.f64 (sin.f64 x) (/.f64 1 (+.f64 1 (cos.f64 x)))))) (*.f64 x x)): 0 points increase in error, 5 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sin.f64 x) (sin.f64 x)) (/.f64 1 (+.f64 1 (cos.f64 x))))) (*.f64 x x)): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto \color{blue}{\frac{\tan \left(x \cdot 0.5\right)}{x} \cdot \frac{\sin x}{x}}
\]
Final simplification0.1
\[\leadsto \frac{\tan \left(x \cdot 0.5\right)}{x} \cdot \frac{\sin x}{x}
\]