Initial program 15.0
\[\frac{\left(\frac{8}{3} \cdot \sin \left(x \cdot 0.5\right)\right) \cdot \sin \left(x \cdot 0.5\right)}{\sin x}
\]
Simplified15.0
\[\leadsto \color{blue}{\left(\sin \left(x \cdot 0.5\right) \cdot \sin \left(x \cdot 0.5\right)\right) \cdot \frac{2.6666666666666665}{\sin x}}
\]
Proof
(*.f64 (*.f64 (sin.f64 (*.f64 x 1/2)) (sin.f64 (*.f64 x 1/2))) (/.f64 8/3 (sin.f64 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (sin.f64 (*.f64 x 1/2)) (sin.f64 (*.f64 x 1/2))) (/.f64 (Rewrite<= metadata-eval (/.f64 8 3)) (sin.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (/.f64 8 3) (sin.f64 x)) (*.f64 (sin.f64 (*.f64 x 1/2)) (sin.f64 (*.f64 x 1/2))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (/.f64 8 3) (*.f64 (sin.f64 (*.f64 x 1/2)) (sin.f64 (*.f64 x 1/2)))) (sin.f64 x))): 38 points increase in error, 29 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 8 3) (sin.f64 (*.f64 x 1/2))) (sin.f64 (*.f64 x 1/2)))) (sin.f64 x)): 26 points increase in error, 28 points decrease in error
Applied egg-rr30.2
\[\leadsto \color{blue}{\frac{1 - \cos x}{\left(\sin x \cdot 0.375\right) \cdot 2}}
\]
Applied egg-rr29.6
\[\leadsto \color{blue}{\log \left(e^{\frac{\tan \left(\frac{x}{2}\right)}{0.75}}\right)}
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{\frac{\tan \left(x \cdot 0.5\right)}{0.75}}
\]
Final simplification0.1
\[\leadsto \frac{\tan \left(x \cdot 0.5\right)}{0.75}
\]