Simplified19.8
\[\leadsto {\left(a \cdot \color{blue}{\mathsf{fma}\left(\cos \left(1 + 0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right), \cos 1, \sin \left(1 + 0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right) \cdot \sin 1\right)}\right)}^{2} + {\left(b \cdot \sin \left(\pi \cdot \frac{angle}{180}\right)\right)}^{2}
\]
Proof
(fma.f64 (cos.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (*.f64 1/180 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) angle))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (PI.f64) angle) 1/180)))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 angle (PI.f64))) 1/180))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite<= associate-*r*_binary64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 14 points increase in error, 15 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 76 points increase in error, 28 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) 1)))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 5 points increase in error, 1 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite=> sub-neg_binary64 (+.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) (neg.f64 1))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (+.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) (Rewrite=> metadata-eval -1)))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 1 (Rewrite=> +-commutative_binary64 (+.f64 -1 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 1 -1) (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (+.f64 (Rewrite=> metadata-eval 0) (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (Rewrite=> +-lft-identity_binary64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (*.f64 angle (PI.f64))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 1/180 (Rewrite<= *-commutative_binary64 (*.f64 (PI.f64) angle))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (PI.f64) angle) 1/180)))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 angle (PI.f64))) 1/180))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite<= associate-*r*_binary64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (sin.f64 1))): 5 points increase in error, 8 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))))) (sin.f64 1))): 33 points increase in error, 25 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) 1)))) (sin.f64 1))): 4 points increase in error, 2 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite=> sub-neg_binary64 (+.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) (neg.f64 1))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (+.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))) (Rewrite=> metadata-eval -1)))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 1 (Rewrite=> +-commutative_binary64 (+.f64 -1 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 1 -1) (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (+.f64 (Rewrite=> metadata-eval 0) (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1) (*.f64 (sin.f64 (Rewrite=> +-lft-identity_binary64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180)))))) (sin.f64 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (cos.f64 1)) (*.f64 (sin.f64 (exp.f64 (log1p.f64 (*.f64 angle (*.f64 (PI.f64) 1/180))))) (sin.f64 1)))): 9 points increase in error, 8 points decrease in error