Initial program 15.1
\[\frac{r \cdot \sin b}{\cos \left(a + b\right)}
\]
Simplified15.1
\[\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}{\cos b \cdot \cos a - \sin b \cdot \sin a}}
\]
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}{\cos a \cdot \cos b - \sin b \cdot \sin a} \cdot r}
\]
Proof
(*.f64 (/.f64 (sin.f64 b) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 b) (sin.f64 a)))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 a) (sin.f64 b))))) r): 0 points increase in error, 0 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))))): 33 points increase in error, 30 points decrease in error
Taylor expanded in b around inf 0.3
\[\leadsto \color{blue}{\frac{\sin b}{\cos a \cdot \cos b - \sin a \cdot \sin b}} \cdot r
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\sin b}{\mathsf{fma}\left(\sin b, -\sin a, \cos a \cdot \cos b\right)}} \cdot r
\]
Proof
(/.f64 (sin.f64 b) (fma.f64 (sin.f64 b) (neg.f64 (sin.f64 a)) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 b) (neg.f64 (sin.f64 a))) (*.f64 (cos.f64 a) (cos.f64 b))))): 4 points increase in error, 6 points decrease in error
(/.f64 (sin.f64 b) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b))))): 0 points increase in error, 0 points decrease in error
Final simplification0.3
\[\leadsto \frac{\sin b}{\mathsf{fma}\left(\sin b, -\sin a, \cos a \cdot \cos b\right)} \cdot r
\]