Initial program 15.1
\[\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.1
\[\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))): 39 points increase in error, 34 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.3
\[\leadsto \color{blue}{\frac{\frac{2.6666666666666665}{\sin x} \cdot \left(1 - \cos x\right)}{2}}
\]
Taylor expanded in x around inf 30.3
\[\leadsto \frac{\color{blue}{2.6666666666666665 \cdot \frac{1 - \cos x}{\sin x}}}{2}
\]
Simplified0.4
\[\leadsto \frac{\color{blue}{2.6666666666666665 \cdot \tan \left(\frac{x}{2}\right)}}{2}
\]
Proof
(*.f64 8/3 (tan.f64 (/.f64 x 2))): 0 points increase in error, 0 points decrease in error
(*.f64 8/3 (Rewrite<= hang-p0-tan_binary64 (/.f64 (-.f64 1 (cos.f64 x)) (sin.f64 x)))): 150 points increase in error, 35 points decrease in error
Final simplification0.4
\[\leadsto \frac{2.6666666666666665 \cdot \tan \left(\frac{x}{2}\right)}{2}
\]