Simplified0.7
\[\leadsto \color{blue}{\sin re \cdot \left(\left({im}^{7} \cdot -0.0001984126984126984 + {im}^{5} \cdot -0.008333333333333333\right) - \left(im + {im}^{3} \cdot 0.16666666666666666\right)\right)}
\]
Proof
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 (pow.f64 im 5) -1/120)) (+.f64 im (*.f64 (pow.f64 im 3) 1/6)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (Rewrite<= *-commutative_binary64 (*.f64 -1/120 (pow.f64 im 5)))) (+.f64 im (*.f64 (pow.f64 im 3) 1/6)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 -1/120 (pow.f64 im 5))) (+.f64 im (*.f64 (pow.f64 im 3) (Rewrite<= metadata-eval (neg.f64 -1/6)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 -1/120 (pow.f64 im 5))) (+.f64 im (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (pow.f64 im 3) -1/6)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 -1/120 (pow.f64 im 5))) (+.f64 im (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/6 (pow.f64 im 3))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 re) (-.f64 (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 -1/120 (pow.f64 im 5))) (Rewrite<= sub-neg_binary64 (-.f64 im (*.f64 -1/6 (pow.f64 im 3)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (sin.f64 re) (+.f64 (*.f64 (pow.f64 im 7) -1/5040) (*.f64 -1/120 (pow.f64 im 5)))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3)))))): 1 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 (pow.f64 im 7) -1/5040) (sin.f64 re)) (*.f64 (*.f64 -1/120 (pow.f64 im 5)) (sin.f64 re)))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 im 7) (*.f64 -1/5040 (sin.f64 re)))) (*.f64 (*.f64 -1/120 (pow.f64 im 5)) (sin.f64 re))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 1 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 -1/5040 (sin.f64 re)) (pow.f64 im 7))) (*.f64 (*.f64 -1/120 (pow.f64 im 5)) (sin.f64 re))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7)))) (*.f64 (*.f64 -1/120 (pow.f64 im 5)) (sin.f64 re))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (Rewrite<= associate-*r*_binary64 (*.f64 -1/120 (*.f64 (pow.f64 im 5) (sin.f64 re))))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (*.f64 -1/120 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 re) (pow.f64 im 5))))) (*.f64 (sin.f64 re) (-.f64 im (*.f64 -1/6 (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5)))) (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 im (sin.f64 re)) (*.f64 (*.f64 -1/6 (pow.f64 im 3)) (sin.f64 re))))): 2 points increase in error, 1 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5)))) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 re) im)) (*.f64 (*.f64 -1/6 (pow.f64 im 3)) (sin.f64 re)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5)))) (-.f64 (*.f64 (sin.f64 re) im) (Rewrite<= associate-*r*_binary64 (*.f64 -1/6 (*.f64 (pow.f64 im 3) (sin.f64 re)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5)))) (-.f64 (*.f64 (sin.f64 re) im) (*.f64 -1/6 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 re) (pow.f64 im 3)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r-_binary64 (+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (-.f64 (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5))) (-.f64 (*.f64 (sin.f64 re) im) (*.f64 -1/6 (*.f64 (sin.f64 re) (pow.f64 im 3))))))): 1 points increase in error, 1 points decrease in error
(+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5))) (*.f64 (sin.f64 re) im)) (*.f64 -1/6 (*.f64 (sin.f64 re) (pow.f64 im 3)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5))) (neg.f64 (*.f64 (sin.f64 re) im)))) (*.f64 -1/6 (*.f64 (sin.f64 re) (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (+.f64 (+.f64 (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (sin.f64 re) im)))) (*.f64 -1/6 (*.f64 (sin.f64 re) (pow.f64 im 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/5040 (*.f64 (sin.f64 re) (pow.f64 im 7))) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/6 (*.f64 (sin.f64 re) (pow.f64 im 3))) (+.f64 (*.f64 -1/120 (*.f64 (sin.f64 re) (pow.f64 im 5))) (*.f64 -1 (*.f64 (sin.f64 re) im)))))): 0 points increase in error, 0 points decrease in error