Initial program 14.9
\[\frac{r \cdot \sin b}{\cos \left(a + b\right)}
\]
Simplified14.9
\[\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-rr0.3
\[\leadsto \frac{r \cdot \sin b}{\color{blue}{\mathsf{fma}\left(\cos b, \cos a, -\sin b \cdot \sin a\right)}}
\]
Taylor expanded in r around 0 0.3
\[\leadsto \color{blue}{\frac{\sin b \cdot r}{\cos a \cdot \cos b - \sin a \cdot \sin b}}
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\sin b}{\mathsf{fma}\left(\cos a, \cos b, \sin b \cdot \left(-\sin a\right)\right)} \cdot r}
\]
Proof
(*.f64 (/.f64 (sin.f64 b) (fma.f64 (cos.f64 a) (cos.f64 b) (*.f64 (sin.f64 b) (neg.f64 (sin.f64 a))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (fma.f64 (cos.f64 a) (cos.f64 b) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (sin.f64 b) (sin.f64 a)))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (fma.f64 (cos.f64 a) (cos.f64 b) (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (sin.f64 a) (sin.f64 b)))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b))))) r): 9 points increase in error, 8 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (sin.f64 b) (/.f64 (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b))) r))): 40 points increase in error, 27 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sin.f64 b) r) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b))))): 36 points increase in error, 37 points decrease in error
Final simplification0.3
\[\leadsto \frac{\sin b}{\mathsf{fma}\left(\cos a, \cos b, \sin b \cdot \left(-\sin a\right)\right)} \cdot r
\]