Simplified0.2
\[\leadsto \color{blue}{\sin x \cdot \left(0.16666666666666666 \cdot {\varepsilon}^{3} - \varepsilon\right) + \cos x \cdot \left(0.041666666666666664 \cdot {\varepsilon}^{4} + -0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\right)}
\]
Proof
(+.f64 (*.f64 (sin.f64 x) (-.f64 (*.f64 1/6 (pow.f64 eps 3)) eps)) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 1/6 (pow.f64 eps 3)) (sin.f64 x)) (*.f64 eps (sin.f64 x)))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 1 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))) (*.f64 eps (sin.f64 x))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x))) (neg.f64 (*.f64 eps (sin.f64 x))))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 eps (sin.f64 x))))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x))))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (*.f64 eps eps))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))) (*.f64 (cos.f64 x) (+.f64 (*.f64 1/24 (pow.f64 eps 4)) (*.f64 -1/2 (Rewrite<= unpow2_binary64 (pow.f64 eps 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 1/24 (pow.f64 eps 4)) (cos.f64 x)) (*.f64 (*.f64 -1/2 (pow.f64 eps 2)) (cos.f64 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x)))) (*.f64 (*.f64 -1/2 (pow.f64 eps 2)) (cos.f64 x)))): 4 points increase in error, 4 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))) (+.f64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x))) (Rewrite<= associate-*r*_binary64 (*.f64 -1/2 (*.f64 (pow.f64 eps 2) (cos.f64 x)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x))) (*.f64 -1/2 (*.f64 (pow.f64 eps 2) (cos.f64 x)))) (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x))) (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 eps 2) (cos.f64 x))) (+.f64 (*.f64 -1 (*.f64 eps (sin.f64 x))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x))))))): 1 points increase in error, 1 points decrease in error
(+.f64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 eps 2) (cos.f64 x))) (*.f64 -1 (*.f64 eps (sin.f64 x)))) (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/24 (*.f64 (pow.f64 eps 4) (cos.f64 x))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 1/6 (*.f64 (pow.f64 eps 3) (sin.f64 x))) (+.f64 (*.f64 -1/2 (*.f64 (pow.f64 eps 2) (cos.f64 x))) (*.f64 -1 (*.f64 eps (sin.f64 x))))))): 0 points increase in error, 0 points decrease in error