Initial program 31.7
\[\frac{1 - \cos x}{x \cdot x}
\]
Applied egg-rr16.5
\[\leadsto \frac{\color{blue}{\left(\sin x \cdot \sin x\right) \cdot \frac{1}{1 + \cos x}}}{x \cdot x}
\]
Simplified16.3
\[\leadsto \frac{\color{blue}{\sin x \cdot \tan \left(\frac{x}{2}\right)}}{x \cdot x}
\]
Proof
(*.f64 (sin.f64 x) (tan.f64 (/.f64 x 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 x) (Rewrite<= hang-0p-tan_binary64 (/.f64 (sin.f64 x) (+.f64 1 (cos.f64 x))))): 27 points increase in error, 37 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (sin.f64 x) (sin.f64 x)) (+.f64 1 (cos.f64 x)))): 14 points increase in error, 29 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (sin.f64 x) (sin.f64 x)) 1)) (+.f64 1 (cos.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 (sin.f64 x) (sin.f64 x)) (/.f64 1 (+.f64 1 (cos.f64 x))))): 16 points increase in error, 14 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}
\]