Initial program 15.3
\[\frac{r \cdot \sin b}{\cos \left(a + b\right)}
\]
Simplified15.3
\[\leadsto \color{blue}{\frac{r \cdot \sin b}{\cos \left(b + a\right)}}
\]
Proof
(/.f64 (*.f64 r (sin.f64 b)) (cos.f64 (+.f64 b a))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 r (sin.f64 b)) (cos.f64 (Rewrite<= +-commutative_binary64 (+.f64 a b)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr15.4
\[\leadsto \frac{r \cdot \sin b}{\color{blue}{\log \left(e^{\cos \left(b + a\right)}\right)}}
\]
Applied egg-rr0.3
\[\leadsto \frac{r \cdot \sin b}{\color{blue}{\cos b \cdot \cos a + \left(-\sin b \cdot \sin a\right)}}
\]
Simplified0.3
\[\leadsto \frac{r \cdot \sin b}{\color{blue}{\mathsf{fma}\left(\sin a, -\sin b, \cos a \cdot \cos b\right)}}
\]
Proof
(fma.f64 (sin.f64 a) (neg.f64 (sin.f64 b)) (*.f64 (cos.f64 a) (cos.f64 b))): 0 points increase in error, 0 points decrease in error
(fma.f64 (sin.f64 a) (neg.f64 (sin.f64 b)) (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 b) (cos.f64 a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 a) (neg.f64 (sin.f64 b))) (*.f64 (cos.f64 b) (cos.f64 a)))): 7 points increase in error, 6 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (sin.f64 b)) (sin.f64 a))) (*.f64 (cos.f64 b) (cos.f64 a))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (sin.f64 b) (sin.f64 a)))) (*.f64 (cos.f64 b) (cos.f64 a))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 b) (cos.f64 a)) (neg.f64 (*.f64 (sin.f64 b) (sin.f64 a))))): 0 points increase in error, 0 points decrease in error
Final simplification0.3
\[\leadsto \frac{r \cdot \sin b}{\mathsf{fma}\left(\sin a, -\sin b, \cos a \cdot \cos b\right)}
\]