Initial program 27.5
\[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\pi \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\pi \cdot \frac{angle}{180}\right)
\]
Simplified27.5
\[\leadsto \color{blue}{\sin \left(\pi \cdot \frac{angle}{180}\right) \cdot \left(\left(-2 \cdot \mathsf{fma}\left(a, a, b \cdot \left(-b\right)\right)\right) \cdot \cos \left(\pi \cdot \frac{angle}{180}\right)\right)}
\]
Proof
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 -2 (fma.f64 a a (*.f64 b (neg.f64 b)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 2)) (fma.f64 a a (*.f64 b (neg.f64 b)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (fma.f64 a a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 b b))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (fma.f64 a a (neg.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 a a) (pow.f64 b 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (pow.f64 b 2))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 2 (neg.f64 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (pow.f64 a 2)) (pow.f64 b 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (pow.f64 a 2))) (pow.f64 b 2))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 b 2) (neg.f64 (pow.f64 a 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= sub-neg_binary64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 19 points increase in error, 16 points decrease in error
(*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr27.8
\[\leadsto \sin \left(\pi \cdot \frac{angle}{180}\right) \cdot \left(\left(-2 \cdot \mathsf{fma}\left(a, a, b \cdot \left(-b\right)\right)\right) \cdot \color{blue}{\sqrt{{\cos \left(\pi \cdot \left(angle \cdot 0.005555555555555556\right)\right)}^{2}}}\right)
\]
Taylor expanded in a around inf 27.6
\[\leadsto \color{blue}{-2 \cdot \left({a}^{2} \cdot \left(\cos \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right) \cdot \sin \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right)\right)\right)}
\]
Simplified19.5
\[\leadsto \color{blue}{a \cdot \left(\left(\cos \left(\pi \cdot \left(angle \cdot 0.005555555555555556\right)\right) \cdot \left(\sin \left(\pi \cdot \left(angle \cdot 0.005555555555555556\right)\right) \cdot a\right)\right) \cdot -2\right)}
\]
Proof
(*.f64 a (*.f64 (*.f64 (cos.f64 (*.f64 (PI.f64) (*.f64 angle 1/180))) (*.f64 (sin.f64 (*.f64 (PI.f64) (*.f64 angle 1/180))) a)) -2)): 0 points increase in error, 0 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (PI.f64) angle) 1/180))) (*.f64 (sin.f64 (*.f64 (PI.f64) (*.f64 angle 1/180))) a)) -2)): 11 points increase in error, 15 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 angle (PI.f64))) 1/180)) (*.f64 (sin.f64 (*.f64 (PI.f64) (*.f64 angle 1/180))) a)) -2)): 0 points increase in error, 0 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/180 (*.f64 angle (PI.f64))))) (*.f64 (sin.f64 (*.f64 (PI.f64) (*.f64 angle 1/180))) a)) -2)): 0 points increase in error, 0 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (*.f64 (sin.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (PI.f64) angle) 1/180))) a)) -2)): 18 points increase in error, 18 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (*.f64 (sin.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 angle (PI.f64))) 1/180)) a)) -2)): 0 points increase in error, 0 points decrease in error
(*.f64 a (*.f64 (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (*.f64 (sin.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/180 (*.f64 angle (PI.f64))))) a)) -2)): 0 points increase in error, 0 points decrease in error
(*.f64 a (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))) a)) -2)): 7 points increase in error, 17 points decrease in error
(*.f64 a (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 a (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))))) -2)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (*.f64 a (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))))) -2)): 1 points increase in error, 1 points decrease in error
(*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a a) (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))))) -2): 44 points increase in error, 17 points decrease in error
(*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))))) -2): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -2 (*.f64 (pow.f64 a 2) (*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
Initial program 34.6
\[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\pi \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\pi \cdot \frac{angle}{180}\right)
\]
Simplified34.6
\[\leadsto \color{blue}{\sin \left(\pi \cdot \frac{angle}{180}\right) \cdot \left(\left(-2 \cdot \mathsf{fma}\left(a, a, b \cdot \left(-b\right)\right)\right) \cdot \cos \left(\pi \cdot \frac{angle}{180}\right)\right)}
\]
Proof
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 -2 (fma.f64 a a (*.f64 b (neg.f64 b)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 2)) (fma.f64 a a (*.f64 b (neg.f64 b)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (fma.f64 a a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 b b))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (fma.f64 a a (neg.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 a a) (pow.f64 b 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 (neg.f64 2) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (pow.f64 b 2))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 2 (neg.f64 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (pow.f64 a 2) (pow.f64 b 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (pow.f64 a 2)) (pow.f64 b 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (pow.f64 a 2))) (pow.f64 b 2))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 b 2) (neg.f64 (pow.f64 a 2))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 (*.f64 2 (Rewrite<= sub-neg_binary64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))) (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180))))): 19 points increase in error, 16 points decrease in error
(*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (PI.f64) (/.f64 angle 180))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle 180)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in b around inf 34.8
\[\leadsto \color{blue}{2 \cdot \left({b}^{2} \cdot \left(\cos \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right) \cdot \sin \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right)\right)\right)}
\]
Taylor expanded in b around 0 34.8
\[\leadsto 2 \cdot \color{blue}{\left(\cos \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right) \cdot \left({b}^{2} \cdot \sin \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right)\right)\right)}
\]
Simplified24.9
\[\leadsto 2 \cdot \color{blue}{\left(\cos \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right) \cdot \left(b \cdot \left(b \cdot \sin \left(0.005555555555555556 \cdot \left(angle \cdot \pi\right)\right)\right)\right)\right)}
\]
Proof
(*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (*.f64 b (*.f64 b (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 b b) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64))))))): 44 points increase in error, 24 points decrease in error
(*.f64 (cos.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (sin.f64 (*.f64 1/180 (*.f64 angle (PI.f64)))))): 0 points increase in error, 0 points decrease in error