Initial program 31.2
\[\frac{1 - \cos x}{x \cdot x}
\]
Applied egg-rr15.9
\[\leadsto \frac{\color{blue}{\left(\sin x \cdot \sin x\right) \cdot \frac{1}{1 + \cos x}}}{x \cdot x}
\]
Simplified15.7
\[\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))))): 31 points increase in error, 34 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (sin.f64 x) (sin.f64 x)) (+.f64 1 (cos.f64 x)))): 22 points increase in error, 17 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))))): 23 points increase in error, 19 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}
\]